This special issue contains extended versions of papers presented at TACAS2011, the seventeenth Annual Conference on TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, held in Saarbrücken, Germany, March 26 - April 3, 2011. 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 seven papers collected in this special issue were invited by the guest editors. The selection was made on the basis of the ranking of the papers by the Program Committee and the opinion of the expert reviewers who assisted the Program Committee. The papers reflect the high level of the conference and represent a wide range of topics including model checking, verification, satisfiability problems, predicate abstraction, and rewriting systems. We are grateful to the authors for their excellent submissions.

All papers were refereed in accordance with the usual high standards of LMCS. We are grateful to the members of the Program Committee of TACAS 2011 and their subreferees as well as to all those who have served as reviewers of the papers submitted to this special issue. We would also like to thank Jiri Adámek, Executive Editor, and Benjamin C. Pierce, Managing Editor, of LMCS for his assistance and guidance.