| Monday, April 7th |
| 10h30 - 12h30 |
TACAS / Room: Amphitheater
Decision procedures and their application in analysis I (chair: Cesare Tinelli)
- Francesco Alberti, Silvio Ghilardi and Natasha Sharygina. Decision Procedures for Flat Array Properties
- Alessandro Armando, Roberto Carbone and Luca Compagna. SATMC: a SAT-based Model Checker for Security-critical Systems
- Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction
- Hassan Eldib, Chao Wang and Patrick Schaumont. SMT-Based Verification of Software Countermeasures against Side-Channel Attacks
|
| 14h00 - 16h00 |
TACAS / Room: Amphitheater
Decision procedures and their application in analysis II (chair: Erika Abraham)
- Bernd Finkbeiner and Leander Tentrup. Detecting Unrealizable Specifications of Distributed Systems
- Arie Gurfinkel, Anton Belov and Joao Marques-Silva. Synthesizing Safe Bit-Precise Invariants
- Michael Huth and Jim Huan-Pu Kuo. PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence
- Ruzica Piskac, Thomas Wies and Damien Zufferey. GRASShopper: Complete Heap Verification with Mixed Specifications
|
| 16h30 - 18h00 |
TACAS / Room: Amphitheater
Complexity and termination analysis (chair: Lenore Zuck)
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs and Jürgen Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs
- Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn. Proving Nontermination via Safety
- Jan Leike and Matthias Heizmann. Ranking Function Templates for Linear Loops
|
| Tuesday, April 8th |
| 10h30 - 12h30 |
TACAS / Room: Amphitheater
Modeling and model checking discrete systems (chair: Bernhard Steffen)
- Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov and A.W. Roscoe. FDR3 - A Modern Refinement Checker for CSP
- Gavin Lowe. Concurrent Depth-First Search Algorithms
- Jan Reineke and Stavros Tripakis. Basic Problems in Multi-View Modeling
- Anton Wijs and Dragan Bosnacki. GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs
|
| Wednesday, April 9th |
| 10h30 - 12h30 |
TACAS / Room: Amphitheater
Timed and hybrid systems I (chair: Christel Baier)
- Dieky Adzkiya, Bart De Schutter and Alessandro Abate. Forward Reachability Computation for Autonomous Max-Plus-Linear Systems
- Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga and Jacques Combaz. Compositional Invariant Generation for Timed Systems
- Khalil Ghorbal and André Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants
|
| 12h30 - 14h00 |
TACAS / Room: Atrium
Tool Demonstrations |
| 15h00 - 16h00 |
TACAS / Room: Amphitheater
Timed and hybrid systems II (chair: Kim G. Larsen)
- Christian Herrera, Bernd Westphal and Andreas Podelski. Quasi-equal Clock Reduction: More Networks, More Queries
- Ting Wang, Jun Sun, Yang Liu, Xinyu Wang and Shanping Li. Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata
|
| 16h30 - 18h00 |
TACAS / Room: Amphitheater
Monitoring, fault detection and identification (chair: Klaus Havelund)
- Marco Bozzano, Alessandro Cimatti, Marco Gario and Stefano Tonetta. Formal design of Fault Detection and Identification components with Temporal Epistemic Logic (nomination for best paper award)
- Normann Decker, Martin Leucker and Daniel Thoma. Monitoring Modulo Theories
- Thomas Reinbacher, Kristin Yvonne Rozier and Johann Schumann. Temporal-Logic Based Runtime Observer Pairs for System Health Mangement of Real-Time Systems
|
| Thursday, April 10th |
| 10h30 - 12h30 |
TACAS / Room: Amphitheater
Competition on software verification (chair: Dirk Beyer)
- Status Report on Software Verification. Dirk Beyer
- BLAST 2.7.2. Pavel Shved, Mikhail Mandrykin, and Vadim Mutilin
- CBMC. Daniel Kröning and Michael Tautschnig
- CPAchecker. Stefan Löwe, Mikhail Mandrykin, and Philipp Wendler
- CPAlien. Petr Muller and Tomas Vojnar
- CSeq-Lazy. Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
- CSeq-MU. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
- ESBMC 1.22. Jeremy Morse, Mikhail Ramalho, Lucas Cordeiro, Denis Nicole, and Bernd Fischer
- FrankenBit. Arie Gurfinkel and Anton Belov
- LLBMC. Stephan Falke, Florian Merz, and Carsten Sinz
- Predator. Kamil Dudka, Petr Peringer, and Tomas Vojnar
- Symbiotic 2. Jiri Slaby and Jan Strejcek
- Threader. Corneliu Popeea and Andrey Rybalchenko
- UFO. Aws Albarghouthi and Arie Gurfinkel
- Ultimate Automizer. Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, and Andreas Podelski
- Ultimate Kojak. Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, and Andreas Podelski
|
| 14h00 - 15h00 |
Room: Amphitheater
TACAS Invited Speaker
Orna Kupferman (Hebrew University Jerusalem, Israel)
Variations on Safety |
| 15h00 - 16h00 |
TACAS / Room: Amphitheater
Specifying and checking linear time properties (chair: Joost-Pieter Katoen)
- Shaull Almagor, Udi Boker and Orna Kupferman. Discounting in LTL
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon and Yann Thierry-Mieg. Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata
|
| 16h00 - 16h30 |
TACAS / Room: Atrium
Tool Demonstrations |
| 16h30 - 18h00 |
TACAS / Room: Amphitheater
Synthesis and learning (chair: Rance Cleaveland)
- Xiaowei Huang and Ron van der Meyden. Symbolic Synthesis for Epistemic Specifications with Observational Semantics
- Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia. Synthesis for Human-in-the-Loop Control Systems
- Oded Maler and Irini Eleftheria Mens. Learning Regular Languages over Large Alphabets
|
| Friday, April 11th |
| 10h30 - 12h30 |
TACAS / Room: Amphitheater
Probabilistic and quantum systems (chair: Nathalie Bertrand)
- Ebrahim Ardeshir-Larijani, Simon Gay and Rajagopal Nagarajan. Verification of Concurrent Quantum Protocols by Equivalence Checking
- Christel Baier, Joachim Klein, Sascha Klueppelholz and Steffen Märcker. Computing Conditional Probabilities in Markovian Models Efficiently (nomination for best paper award)
- Klaus Dräger, Vojtech Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems
- Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Precise Approximations of the Probability Distribution of a Markov Process in Time: an Application to Probabilistic Invariance
|
| 14h00 - 16h00 |
TACAS / Room: Amphitheater
Tool demonstrations (chair: Saddek Bensalem)
- Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gomez-Zamalloa, Enrique Martin-Martin, German Puebla and Guillermo Román-Díez. SACO: Static Analyzer for Concurrent Objects
- Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. VeriMAP: A Tool for Verifying Programs through Transformations
- Bert van Beek, Wan Fokkink, Dennis Hendriks, Albert Hofkamp, Jasen Markovski, Asia van de Mortel-Fronczak and Michel Reniers. CIF 3: Model-based Engineering of Supervisory Controllers
- Rafael Caballero, Enrique Martin-Martin, Adrian Riesco and Salvador Tamarit. EDD: A Declarative Debugger for Sequential Erlang Programs
- Vincent Cheval. APTE: an Algorithm for Proving Trace Equivalence
- Arnd Hartmanns and Holger Hermanns. The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification
- Antti Siirtola. Bounds2: A Tool for Compositional Multi-Parametrised Verification
|
| 16h30 - 18h00 |
TACAS / Room: Amphitheater
Case studies (chair: Ylies Falcone)
- Jaap Boender and Claudio Sacerdoti Coen. On the Correctness of a Branch Displacement Algorithm
- Christian Von Essen and Dimitra Giannakopoulou. Analyzing the Next Generation Airborne Collision Avoidance System (nomination for best paper award)
- Erwan Jahier, Simplice Djoko-Djoko, Eric Lafont and Chaouki Maiza. Environment-Model Based Testing of Control Systems: Case Studies
|