Abstract is missing.
- A Logical Analysis of Framing for Specifications with Pure Method CallsAnindya Banerjee, David A. Naumann. 3-20 [doi]
- Efficient Refinement Checking in VCCSumesh Divakaran, Deepak D'Souza, Nigamanth Sridhar. 21-36 [doi]
- Formalizing Semantics with an Automatic Program VerifierMartin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. 37-51 [doi]
- The KeY Platform for Verification and Analysis of Java ProgramsWolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich. 55-71 [doi]
- A Verification Condition VisualizerMadiha Jami, Andrew Ireland. 72-86 [doi]
- Formal Modeling and Verification of CloudProxyWei Yang Tan, Rohit Sinha, John L. Manferdelli, Sanjit A. Seshia. 87-104 [doi]
- Using Promela in a Fully Verified Executable LTL Model CheckerRené Neumann. 105-114 [doi]
- Store Buffer Reduction with MMUsGeng Chen, Ernie Cohen, Mikhail Kovalev. 117-132 [doi]
- Separation Kernel Verification: The Xtratum Case StudyDavid Sanán, Andrew Butterfield, Mike Hinchey. 133-149 [doi]
- Separation Algebras for C Verification in CoqRobbert Krebbers. 150-166 [doi]
- Automatically Verified Implementation of Data Structures Based on AVL TreesMartin Clochard. 167-180 [doi]
- A Model for Capturing and Replaying Proof StrategiesLeo Freitas, Cliff B. Jones, Andrius Velykis, Iain Whiteside. 183-199 [doi]
- A Certifying Frontend for (Sub)polyhedral Abstract DomainsAlexis Fouilhé, Sylvain Boulmé. 200-215 [doi]
- Certification of Nontermination Proofs Using Strategies and Nonlooping DerivationsJulian Nagele, René Thiemann, Sarah Winkler. 216-232 [doi]
- Parameterized Model-Checking of Timed Systems with Conjunctive GuardsLuca Spalazzi, Francesco Spegni. 235-251 [doi]
- Timed Refinement for Verification of Real-Time Object Code ProgramsMohana Asha Latha Dubasi, Sudarshan K. Srinivasan, Vidura Wijayasekara. 252-269 [doi]
- What Gives? A Hybrid Algorithm for Error Trace ExplanationVijayaraghavan Murali, Nishant Sinha, Emina Torlak, Satish Chandra. 270-286 [doi]