TACAS 2014 accepted papers

Research papers

Francesco Alberti, Silvio Ghilardi and Natasha Sharygina. Decision Procedures for Flat Array Properties.

Shaull Almagor, Udi Boker and Orna Kupferman. Discounting in LTL.

Ebrahim Ardeshir-Larijani, Simon Gay and Rajagopal Nagarajan. Verification of Concurrent Quantum Protocols by Equivalence Checking.

Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga and Jacques Combaz. Compositional Invariant Generation for Timed Systems.

Christel Baier, Joachim Klein, Sascha Klueppelholz and Steffen Märcker. Computing Conditional Properties in Markovian Models Efficiently.

Marco Bozzano, Alessandro Cimatti, Marco Gario and Stefano Tonetta. Formal design of Fault Detection and Identification components with Temporal Epistemic Logic.

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.

Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction.

Normann Decker, Martin Leucker and Daniel Thoma. Monitoring Modulo Theories.

Klaus Dräger, Vojtech Forejt, Marta Kwiatkowska, David Parker and Mateusz Ujma. Permissive Controller Synthesis for Probabilistic Systems.

Hassan Eldib, Chao Wang and Patrick Schaumont. SMT-Based Verification of Software Countermeasures against Side-Channel Attacks.

Bernd Finkbeiner and Leander Tentrup. Detecting Unrealizable Specifications of Distributed Systems.

Khalil Ghorbal and André Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants.

Arie Gurfinkel, Anton Belov and Joao Marques-Silva. Synthesizing Safe Bit-Precise Invariants.

Christian Herrera, Bernd Westphal and Andreas Podelski. Quasi-equal Clock Reduction: More Networks, More Queries.

Xiaowei Huang and Ron van der Meyden. Symbolic Synthesis for Epistemic Specifications with Observational Semantics.

Jan Leike and Matthias Heizmann. Ranking Function Templates for Linear Loops.

Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia. Synthesis for Human-in-the-Loop Control Systems.

Gavin Lowe. Concurrent Depth-First Search Algorithms.

Oded Maler and Irini Eleftheria Mens. Learning Regular Languages over Large Alphabets.

Thomas Reinbacher, Kristin Yvonne Rozier and Johann Schumann. Temporal-Logic Based Runtime Observer Pairs for System Health Mangement of Real-Time Systems.

Jan Reineke and Stavros Tripakis. Basic Problems in Multi-View Modeling.

Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon and Yann Thierry-Mieg. Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata.

Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Precise Approximations of the Probability Distribution of a Markov Process in Time: an Application to Probabilistic Invariance.

Ting Wang, Jun Sun, Yang Liu, Xinyu Wang and Shanping Li. Language Inclusion Checking for Timed Automata.

Case study papers

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.

Erwan Jahier, Simplice Djoko-Djoko, Eric Lafont and Chaouki Maiza. Environment-Model Based Testing of Control Systems: Case Studies.

Regular tool papers

Dieky Adzkiya, Bart De Schutter and Alessandro Abate. Forward Reachability Computation for Autonomous Max-Plus-Linear Systems.

Alessandro Armando, Roberto Carbone and Luca Compagna. SATMC: a SAT-based Model Checker for Security-critical Systems.

Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov and A.W. Roscoe. FDR3 — A Modern Refinement Checker for CSP.

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.

Anton Wijs and Dragan Bosnacki. GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs.

Tool demonstration papers

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.