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