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.