Verified software: Theories, tools and experiments

The importance of verification for software products is being increasingly appreciated in industry, although still not to the level to make it a standard approach to high quality software in industry. Since 2005, a global initiative has been underway, started by eminent researchers in both industry and academia, with the aim of establishing and disseminating a culture of software verification from first principles by means of theories, tools and experiments. This special section contains a selection of contributions originally presented at the 2008 Workshop on Tools at VSTTE 2008, the conference on Verified Software: Theories, Tools and Experiments, in Toronto. The VSTTE series of conferences and workshops focuses on the challenge of verifying software systems. Within VSTTE, the scope of the Tools workshop are implementations and enabling techniques for program verifiers, which are important ingredients for the dissemination of principles and techniques among industrial practitioners. This special section complements a sister special section of the Journal on Formal Aspects of computing, Springer. While the FACJ papers address more foundational aspects of tool-based verification and tool construction, the present section presents two toolsets, reflections on usability for verification tools and a novel abstraction technique.