Verified Software: Theories, Tools, Experiments

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?.