| Monday, April 4th |
| 10h30 - 12h30 |
TACAS / Room: Blauwe Zaal
Abstraction and Verification I (Chair: Arie Gurfinkel)
- Alexey Bakhirkin and Nir Piterman. Finding Recurrent Sets with Backwards Analysis and Trace Partitioning
- Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier (EATCS award nominee)
- Caterina Urban, Arie Gurfinkel and Temesghen Kahsai. Synthesizing Ranking Functions from Bits and Pieces
- Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
|
| 14h00 - 16h00 |
TACAS / Room: Blauwe Zaal
Probabilistic and Stochastic Systems I (Chair: Bernhard Steffen)
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. Efficient Syntax-driven Lumping of Differential Equations
- Przemysław Daca, Thomas Henzinger, Jan Křetínský and Tatjana Petrov. Faster Statistical Model Checking for Unbounded Temporal Properties (EATCS award nominee)
- Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu and Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs
- Sadegh Soudjani, Rupak Majumdar and Alessandro Abate. Safety Verification of Continuous-Space Pure Jump Markov Processes
|
| 16h30 - 18h00 |
TACAS / Room: Blauwe Zaal
Synthesis (Chair: Rupak Majumdar)
- Christof Löding, Parthasarathy Madhusudan and Daniel Neider. Abstract Learning Frameworks for Synthesis
- Parthasarathy Madhusudan, Daniel Neider and Shambwaditya Saha. Synthesizing Piece-wise Functions by Learning Classifiers (EASST award nominee)
- Daniel Neider and Ufuk Topcu. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
|
| Tuesday, April 5th |
| 10h30 - 12h30 |
TACAS / Room: Blauwe Zaal
Probabilistic and Stochastic Systems II (Chair: Kim G. Larsen)
- Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov and Sriram Sankaranarayanan. Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
- Kim G. Larsen, Marius Mikucionis, Marco Muniz, Jiri Srba and Jakob Haahr Taankvist. Online and Compositional Learning of Controllers with Application to Floor Heating
- Aleksandar Chakarov, Yuen-Lam Voronin and Sriram Sankaranarayanan. Deductive Proofs of Almost Sure Persistence and Recurrence Properties
- Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns and Rupak Majumdar. Probabilistic CTL* : The Deductive Way
|
| 15h30 - 18h00 |
TACAS / Room: Blauwe Zaal
Tools I (Chair: Dirk Beyer)
- Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi and Zhibin Yang. Parametric Runtime Verification of C Programs
- Alexander Faithfull, Jesper Bengtson, Tassi Enrico and Carst Tankink. Coqoon: an IDE for interactive proof development in Coq (EAPLS award nominee)
- Tom van Dijk and Jaco van de Pol. Multi-core symbolic bisimulation minimisation
- Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker and David Müller. Advances in Symbolic Probabilistic Model Checking with PRISM
- Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim and Marta Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
|
TACAS / Zwarte Doos
Tools II (Chair: Radu Mateescu)
- Souha Ben Rayana, Marius Bozga, Saddek Bensalem and Jacques Combaz. RTD-Finder: A Tool for Compositional Verification of Real-Time Component-based Systems
- Martin Avanzini, Georg Moser and Michael Schaper. TcT: Tyrolean Complexity Tool
- Maria Christakis, Rustan Leino, Peter Müller and Valentin Wüstholz. Integrated Environment for Diagnosing Verification Errors
- Kasper Luckow, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Marko Dimjasevic, Zvonimir Rakamaric, Vishwanath Raman and Temesghen Kahsai. JDart: A Dynamic Symbolic Analysis Framework
- [Tool demo] Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf and Nir Piterman. T2: Temporal Property Verification
|
| Wednesday, April 6th |
| 10h00 - 10h30 |
TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1 |
| 10h30 - 12h30 |
TACAS / Room: Blauwe Zaal
Concurrency (Chair: Radu Calinescu)
- Cédric Favre, Hagen Völzer and Peter Müller. Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-ChoiceWorkflow Nets)
- Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously (EATCS award nominee)
- Constantin Enea and Azadeh Farzan. On Atomicity in Presence of Non-atomic Writes
- Daniel Poetzl and Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
|
| 12h30 - 14h00 |
TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1 |
| 14h00 - 16h00 |
TACAS / Room: Blauwe Zaal
Tool Demos (Chair: Radu Mateescu)
- Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli and Gianni Zampedri. The xSAP Safety Analysis Platform
- Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals
- Sung-Shik T.Q. Jongmans and Farhad Arbab. PrDK: Protocol Programming with Automata
- Hugues Evrard. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
- Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games
- Luca Compagna, Daniel Ricardo Dos Santos, Serena Elisa Ponta and Silvio Ranise. Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-sensitive Business Processes
- Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering
- Rajdeep Mukherjee, Michael Tautschnig and Daniel Kroening. v2c - A Verilog to C Translator Tool
|
| 16h00 - 16h30 |
TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1 |
| 16h30 - 18h00 |
TACAS / Room: Blauwe Zaal
Abstraction and Verification II (Chair: Parosh Abdulla)
- Kedar S. Namjoshi and Richard J. Trefler. Parameterized Compositional Model Checking
- Jan Friso Groote and Anton Wijs. An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
- Sicun Gao and Damien Zufferey. Interpolants in Nonlinear Theories over the Reals
|
| Thursday, April 7th |
| 10h00 - 10h30 |
TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1 |
| 10h30 - 12h30 |
TACAS / Room: Blauwe Zaal
Abstraction and Verification III (Chair: Marsha Chechik)
- Filip Konecny. PTIME Computation of Transitive Closures of Octagonal Relations
- Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. Scalable Verification of Linear Controller Software
- Pallavi Maiya, Rahul Gupta, Aditya Kanade and Rupak Majumdar. Partial Order Reduction for Event-driven Multi-threaded Programs
- Mohamed Faouzi Atig, K. Narayan Kumar and Prakash Saivasan. Acceleration in Multi-Pushdown systems
|
| 12h30 - 14h00 |
TACAS Tool Market / Room: Outside Blauwe Zaal, floor 1 |
| 14h00 - 16h00 |
TACAS / Room: Blauwe Zaal
Languages and Automata (Chair: Nir Piterman)
- Ricardo Almeida, Lukas Holik and Richard Mayr. Minimization of Nondeterministic Tree Automata
- Dogan Ulus, Thomas Ferrere, Eugene Asarin and Oded Maler. Online Timed Pattern Matching using Derivatives
- Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan. Hybridization based CEGAR for Hybrid Automata with Affine Dynamics
- František Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejček and Ming-Hsien Tsai. Complementing Semi-deterministic Büchi Automata
|
TACAS / Room: CZ 7
Competition on Software Verification - Open Jury Meeting and Technical Discussion (Chair: Dirk Beyer) Starts at 15:00 |
| 16h30 - 18h00 |
TACAS / Room: CZ 2
Security (Chair: Marsha Chechik)
- Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
- Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker and Sharon Shoham. Some Complexity Results for Stateful Network Verification
|
TACAS / Room: CZ 8
Optimization (Chair: Jean-François Raskin)
- Julien Lange and Nobuko Yoshida. Characteristic Formulae for Session Type
- Alexander Nadel and Vadim Ryvchin. Bit-Vector Optimization
- Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz and Daniel Thoma. Runtime Monitoring with Union-Find Structures
|
TACAS / Room: CZ 7
Competition on Software Verification - Presentation (Chair: Dirk Beyer) |