Tools and Algorithms for the Construction and Analysis of Systems

1. Front Matter

   PDF

2. Invited Contribution

   1. Variations on Safety

      • Orna Kupferman

      Pages 1-14

3. Decision Procedures and Their Application in Analysis

   1. Decision Procedures for Flat Array Properties

      • Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

      Pages 15-30

   2. SATMC: A SAT-Based Model Checker for Security-Critical Systems

      • Alessandro Armando, Roberto Carbone, Luca Compagna

      Pages 31-45

   3. IC3 Modulo Theories via Implicit Predicate Abstraction

      • Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta

      Pages 46-61

   4. SMT-Based Verification of Software Countermeasures against Side-Channel Attacks

      • Hassan Eldib, Chao Wang, Patrick Schaumont

      Pages 62-77

   5. Detecting Unrealizable Specifications of Distributed Systems

      • Bernd Finkbeiner, Leander Tentrup

      Pages 78-92

   6. Synthesizing Safe Bit-Precise Invariants

      • Arie Gurfinkel, Anton Belov, Joao Marques-Silva

      Pages 93-108

   7. PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence

      • Michael Huth, Jim Huan-Pu Kuo

      Pages 109-123

   8. GRASShopper

      • Ruzica Piskac, Thomas Wies, Damien Zufferey

      Pages 124-139

4. Complexity and Termination Analysis

   1. Alternating Runtime and Size Complexity Analysis of Integer Programs

      • Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl

      Pages 140-155

   2. Proving Nontermination via Safety

      • Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter O’Hearn

      Pages 156-171

   3. Ranking Templates for Linear Loops

      • Jan Leike, Matthias Heizmann

      Pages 172-186

5. Modeling and Model Checking Discrete Systems

   1. FDR3 — A Modern Refinement Checker for CSP

      • Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, Andrew W. Roscoe

      Pages 187-201

   2. Concurrent Depth-First Search Algorithms

      • Gavin Lowe

      Pages 202-216

   3. Basic Problems in Multi-View Modeling

      • Jan Reineke, Stavros Tripakis

      Pages 217-232

   4. GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs

      • Anton Wijs, Dragan Bošnački

      Pages 233-247

6. Timed and Hybrid Systems

   1. Forward Reachability Computation for Autonomous Max-Plus-Linear Systems

      • Dieky Adzkiya, Bart De Schutter, Alessandro Abate

      Pages 248-262

   2. Compositional Invariant Generation for Timed Systems

      • Lacramioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz

      Pages 263-278

   3. Characterizing Algebraic Invariants by Differential Radical Invariants

      • Khalil Ghorbal, André Platzer

      Pages 279-294

This book constitutes the proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, which took place in Grenoble, France, in April 2014, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. The total of 42 papers included in this volume, consisting of 26 research papers, 3 case study papers, 6 regular tool papers and 7 tool demonstrations papers, were carefully reviewed and selected from 161 submissions. In addition the book contains one invited contribution. The papers are organized in topical sections named: decision procedures and their application in analysis; complexity and termination analysis; modeling and model checking discrete systems; timed and hybrid systems; monitoring, fault detection and identification; competition on software verification; specifying and checking linear time properties; synthesis and learning; quantum and probabilistic systems; as well as tool demonstrations and case studies.

• algorithms
• automata theory
• complexity
• decision procedures
• dynamic analysis
• formal methods
• hardware verification
• hybrid models
• logic
• model checking
• models of computation
• probabilistic systems
• program specifications
• programming languages
• realtime
• software engineering
• softwrae verification
• static analysis
• theorem proving
• timed models

• RWTH Aachen, Germany

  Erika Ábrahám

• Jet Propulsion Laboratory, California Institute of Technology, USA

  Klaus Havelund

Policies and ethics