20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014)


Editors: Erika Abraham, Klaus Havelund

This special issue of the journal Logical Methods in Computer Science (LMCS) contains revised and extended versions of seven papers presented at the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), held in Grenoble, France during April 7-11, 2014, as part of the Joint European Conferences on Theory and Practice of Software (ETAPS).

TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The research areas covered by TACAS include, but are not limited to, formal methods, software and hardware specification and verification, static analysis, dynamic analysis, model checking, theorem proving, decision procedures, real-time, hybrid and stochastic systems, communication protocols, programming languages, and software engineering. TACAS provides a venue where common problems, heuristics, algorithms, data structures, and methodologies in these areas can be discussed and explored.

The papers collected in this special issue have been invited by the guest editors amongst the top papers presented at TACAS'14 based on their relevance to LMCS. We are grateful to all authors for their contributions and to the reviewers of TACAS'14 and of this special issue for their thorough and valuable work.

Erika Ábrahám and Klaus Havelund
Special Issue Editors TACAS’14

1. Ranking Templates for Linear Loops

Leike, Jan ; Heizmann, Matthias.
We present a new method for the constraint-based synthesis of termination arguments for linear loop programs based on linear ranking templates. Linear ranking templates are parameterized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. Our […]

2. Permissive Controller Synthesis for Probabilistic Systems

Drager, Klaus ; Forejt, Vojtech ; Kwiatkowska, Marta ; Parker, David ; Ujma, Mateusz.
We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty […]

3. Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions

Soudjani, Sadegh Esmaeil Zadeh ; Abate, Alessandro.
The goal of this work is to formally abstract a Markov process evolving in discrete time over a general state space as a finite-state Markov chain, with the objective of precisely approximating its state probability distribution in time, which allows for its approximate, faster computation by that […]

4. Detecting Unrealizability of Distributed Fault-tolerant Systems

Finkbeiner, Bernd ; Tentrup, Leander.
Writing formal specifications for distributed systems is difficult. Even simple consistency requirements often turn out to be unrealizable because of the complicated information flow in the distributed system: not all information is available in every component, and information transmitted from […]

5. Learning Regular Languages over Large Ordered Alphabets

Mens, Irini-Eleftheria ; Maler, Oded.
This work is concerned with regular languages defined over large alphabets, either infinite or just too large to be expressed enumeratively. We define a generic model where transitions are labeled by elements of a finite partition of the alphabet. We then extend Angluin's L* algorithm for learning […]

6. Compositional Verification for Timed Systems Based on Automatic Invariant Generation

Astefanoaei, Lacramioara ; Rayana, Souha Ben ; Bensalem, Saddek ; Bozga, Marius ; Combaz, Jacques.
We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we […]

7. Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic

Bozzano, Marco ; Cimatti, Alessandro ; Gario, Marco ; Tonetta, Stefano.
Autonomous critical systems, such as satellites and space rovers, must be able to detect the occurrence of faults in order to ensure correct operation. This task is carried out by Fault Detection and Identification (FDI) components, that are embedded in those systems and are in charge of […]