Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Shankar, Natarajan (Editor), Woodcock, Jim (Editor)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg, 2008.
• Series: Lecture Notes in Computer Science, 5295
• Subjects: Computer science.; Computer programming.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Computers.; Computer Science.; Software Engineering.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.; Programming Techniques.; Models and Principles.

This volume contains the proceedings of the second working conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2008, held in Toronto, Canada, in October 2008. The 16 papers presented together with 4 invited talks were carefully revised and selected for inclusion in the book. Thi...

Table of Contents:

• Keynote Talks (Abstracts)
• Readable Formal Proofs
• From Verification to Synthesis
• Verification, Least-Fixpoint Checking, Abstraction
• Combining Tests and Proofs
• Logics
• Propositional Dynamic Logic for Recursive Procedures
• Mapped Separation Logic
• Unguessable Atoms: A Logical Foundation for Security
• Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems
• Tools
• JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML
• Incremental Benchmarks for Software Verification Tools and Techniques
• Case Studies
• Verified Protection Model of the seL4 Microkernel
• Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic
• Bounded Verification of Voting Software
• Methodology
• Expression Decomposition in a Rely/Guarantee Context
• A Verification Approach for System-Level Concurrent Programs
• Boogie Meets Regions: A Verification Experience Report
• Flexible Immutability with Frozen Objects
• Verisoft
• The Verisoft Approach to Systems Verification
• Formal Functional Verification of Device Drivers
• Verified Process-Context Switch for C-Programmed Kernels
• Paper from VSTTE 2005
• Where Is the Value in a Program Verifier?.