 |
 |
Fifteenth International Conference on "Tools and Algorithms for the Construction and Analysis of Systems TACAS 2009"
2009
Editor: Anna Philippou
This special issue contains extended versions of a selection of four articles presented at the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) held on 22 29 March 2009, in York, UK.
TACAS is a forum for researchers, developers and users interested in rigorously-based tools and algorithms for the construction and analysis of systems. The conference serves to bridge the gaps between different communities that share common interests in, and techniques for, tool development and its algorithmic foundations. TACAS is a member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS), which is the primary European forum for academic and industrial researchers working on topics relating to Software Science.
The four papers collected in this special issue were invited by the guest editors amongst the top papers presented at TACAS 2009 based on their relevance to the Logical Methods in Computer Science journal. All submissions underwent a new and thorough reviewing and revision process, in accordance with the high standards of LMCS.
The issue begins with the article Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads by Mohamed Faouzi Atig, Ahmed Bouajjani and Shaz Qadeer. In this paper, the authors propose a new definition of context-bounded analysis of concurrent programs in the presence of dynamic thread creation and they establish decidability and complexity results for the analysis induced by several variants of this definition.
In the next article entitled Ground Interpolation for the Theory of Equality by Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic and Cesare Tinelli, the authors present a novel algorithm for generating ground interpolants for the theory of equality and uninterpreted functions using colored congruence graphs. Furthermore, the authors formulate the interpolation problem as a two-player cooperative game and they show that the proposed interpolation method for the theory of equality constitutes a theory-specific implementation of this general game.
Grigore Rosu and Feng Chens contribution Semantics and Algorithms for Parametric Monitoring provides a theoretical foundation for parametric monitoring. It investigates the problem of analyzing parametric execution traces against formally specified correctness requirements and in doing this it proposes algorithms for the problem which are experimentally evaluated in the context of checking properties for Java programs.
Finally in their article Büchi Complementation and Size-Change Termination, Seth Fogarty and Moshe Y. Vardi investigate the links that exist between two important problems in theoretical computer science and computer aided-verification: the language inclusion problem for Büchi automata and the notion of size-change termination. They demonstrate that the Ramsey-based size-change termination algorithm is a specialized realization of the Ramsey-based complementation construction. With this link established, they compare rank-based and Ramsey-based tools on the domain of size-change termination problems.
We would like to thank all authors for their contributions and the referees for their thorough and valuable reports. Finally, we would like to thank Jirí Adámek, Executive Editor, Benjamin C. Pierce, Managing Editor, and Andrzej Tarlecki, Editor, of LMCS for their assistance and guidance.
Guest Editors and PC Co-Chairs of TACAS 2009
1. Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads
Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis explores all behaviors of a concurrent program up to some fixed number of context switches between threads. This definition is inadequate for programs that create threads dynamically because bounding the number of context switches in a computation also bounds the number of threads involved in the computation. In this paper, we propose a more general definition of context-bounded analysis useful for programs with dynamic thread creation. The idea is to bound the number of context switches for each thread instead of bounding the number of switches of all threads. We consider several variants based on this new definition, and we establish decidability and complexity results for the analysis induced by them.
2. Ground interpolation for the theory of equality
Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By working with graphs, rather than at the level of individual proof steps, we are able to derive interpolants that are pleasingly simple (conjunctions of Horn clauses) and smaller than those generated by other tools. Our interpolation method can be seen as a theory-specific implementation of a cooperative interpolation game between two provers. We present a generic version of the interpolation game, parametrized by the theory T, and define a general method to extract runs of the game from proofs in T and then generate interpolants from these runs.
3. Semantics and Algorithms for Parametric Monitoring
Analysis of execution traces plays a fundamental role in many program analysis approaches, such as runtime verification, testing, monitoring, and specification mining. Execution traces are frequently parametric, i.e., they contain events with parameter bindings. Each parametric trace usually consists of many meaningful trace slices merged together, each slice corresponding to one parameter binding. This gives a semantics-based solution to parametric trace analysis. A general-purpose parametric trace slicing technique is introduced, which takes each event in the parametric trace and dispatches it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis technique, by applying the later on each trace slice. As an instance, a parametric property monitoring technique is then presented. The presented parametric trace slicing and monitoring techniques have been implemented and extensively evaluated. Measurements of runtime overhead confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing parametric trace monitoring systems.
4. Büchi Complementation and Size-Change Termination
We compare tools for complementing nondeterministic Büchi automata with a recent termination-analysis algorithm. Complementation of Büchi automata is a key step in program verification. Early constructions using a Ramsey-based argument have been supplanted by rank-based constructions with exponentially better bounds. In 2001 Lee et al. presented the size-change termination (SCT) problem, along with both a reduction to Büchi automata and a Ramsey-based algorithm. The Ramsey-based algorithm was presented as a more practical alternative to the automata-theoretic approach, but strongly resembles the initial complementation constructions for Büchi automata. We prove that the SCT algorithm is a specialized realization of the Ramsey-based complementation construction. To do so, we extend the Ramsey-based complementation construction to provide a containment-testing algorithm. Surprisingly, empirical analysis suggests that despite the massive gap in worst-case complexity, Ramsey-based approaches are superior over the domain of SCT problems. Upon further analysis we discover an interesting property of the problem space that both explains this result and provides a chance to improve rank-based tools. With these improvements, we show that theoretical gains in efficiency of the rank-based approach are mirrored in empirical performance.