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.