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