ETAPS 2014: 5-13 April 2014, Grenoble, France

TACAS 2014 programme

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