Accepted Papers
Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter Schmitt and Mattias Ulbrich. The KeY Platform for Verification and Analysis of Java Programs
Martin Clochard, Jean-Christophe Filliatre, Claude Marché and Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier
Madiha Jami and Andrew Ireland. A Verification Condition Visualizer
Martin Clochard. Automatically verified implementation of data structures based on AVL trees (SHORT)
David Sanan, Andrew Butterfield and Michael Hinchey. Separation Kernel Verification: the XtratuM Case Study
Alexis Fouilhe and Sylvain Boulmé. A certifying frontend for (sub)polyhedral abstract domains
Anindya Banerjee and David Naumann. A logical analysis of framing for specifications with pure method calls
Leo Freitas, Cliff B. Jones, Andrius Velykis and Iain Whiteside. A Model for Capturing and Replaying Proof Strategies
Sumesh Divakaran, Deepak D'Souza and Nigamanth Sridhar. Efficient Refinement Checking in VCC
René Neumann. Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
Robbert Krebbers. Separation algebras for C verification in Coq
Julian Nagele, René Thiemann and Sarah Winkler. Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
Mikhail Kovalev, Ernie Cohen and Geng Chen. Store Buffer Reduction with MMUs
Mohana Asha Latha Dubasi, Sudarshan Srinivasan and Vidura Wijayasekara. Timed Refinements for Verification of Real-Time Object Code Programs
Luca Spalazzi and Francesco Spegni. Model Checking Parameterized Timed Systems
Wei Yang Tan, Rohit Sinha, John Manferdelli and Sanjit Seshia. Formal Modeling and Verification of CloudProxy
Vijayaraghavan Murali, Nishant Sinha, Emina Torlak and Satish Chandra. A Hybrid Algorithm for Error Trace Explanation