This volume contains the proceedings of the 17th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS
2011). TACAS 2011 took place in Saarbr¨ucken, Germany, March 28–31, 2011,
as part of the 14th European Joint Conferences on Theory and Practice of Software
(ETAPS 2011), whose aims, organization, and history are presented in the
foreword of this volume by the ETAPS Steering Committee Chair, Vladimiro
Sassone.
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 tool development and its algorithmic foundations. The
research areas covered by such communities include, but are not limited to, formal
methods, software and hardware verification, static analysis, programming
languages, software engineering, real-time systems, communications protocols,
and biological systems. The TACAS forum provides a venue for such communities
at which common problems, heuristics, algorithms, data structures, and methodologies
can be discussed and explored. TACAS aims to support researchers in
their quest to improve the usability, utility, flexibility, and efficiency of tools
and algorithms for building systems. Tool descriptions and case studies with a
conceptual message, as well as theoretical papers with clear relevance for tool
construction, are all encouraged. The specific topics covered by the conference
include, but are not limited to, the following: specification and verification techniques
for finite and infinite-state systems, software and hardware verification,
theorem proving and model checking, system construction and transformation
techniques, static and run-time analysis, abstraction techniques for modeling
and validation, compositional and refinement-based methodologies, testing and
test-case generation, analytical techniques for safety, security, or dependability,
analytical techniques for real-time, hybrid, or stochastic systems, integration of
formal methods and static analysis in high-level hardware design or software
environments, tool environments and tool architectures, SAT and SMT solvers,
and applications and case studies.
