Verified Software: Theories, Tools, Experiments

This volume contains the papers presented at the Second Working Conference on Veri?ed Software: Theories, Tools, and Experiments held in Toronto d- ing October 6-9, 2008. This followed a successful working conference held in Zurich in 2005, also published in Lecture Notes in Computer Science as volume 4171 (DOI 10.1007/978-3-540-69149-5).The second conference formally inau- ratedtheVeri?edSoftwareInitiative(VSI),a15-year,co-operative,international project directed at the scienti?c challenges of large-scale software veri?cation. The scope of the cooperative e?ort includes the sharing and interoperability of tools, the alignment of theory and practice, the identi?cation of challenge problems, the construction of benchmark suites, and the execution of large-scale experiments. The conference was open to everyone interested in participating actively in the VSI e?ort. The scope of the VSTTE conferences includes all aspects of veri?ed software, covering theoretical as well as experimental work: - type systems - requirements modelling - computer security - speci?cation languages - static analyzers - speci?cation case studies - dynamic analyzers - formal calculi - model checkers - programming languages - language semantics - theorem provers - software design methods - satis?ability checkers - software testing - benchmarks - automatic code generation - challenge problems - re?nement methodologies - integrated veri?cation environments The conference was addressed by four keynote speakers: - John Reynolds (Carnegie Mellon University) - Moshe Vardi (Rice University) - Andreas Podelski (University of Freiburg) - Sriram Rajamani (Microsoft Research) Two invited tutorials were given by: - Eric Hehner (University of Toronto) Practical Predicative Programming Primer