Accepted Papers

Title Authors
Verifying Two Lines of C with Why3: an Exercise in Program VerificationJean-Christophe Filliatre
Infeasible Code DetectionCristiano Bertolini, Martin Schäf and Pascal Schweitzer
Development and Evaluation of LAV: an SMT-Based Error Finding PlatformMilena Vujosevic-Janicic and Viktor Kuncak
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++Van Tang Nguyen
A Certified Multi-prover Verification Condition GeneratorPaolo Herms, Claude Marché and Benjamin Monate
Formalized Verification of Snapshotable Trees: Separation and SharingHannes Mehnert, Filip Sieczkowski, Lars Birkedal and Peter Sestoft
Termination Analysis of Imperative Programs Using Bitvector ArithmeticStephan Falke, Deepak Kapur and Carsten Sinz
Comparing Verification Condition Generation with Symbolic Execution: an Experience ReportIoannis T. Kassios, Peter Müller and Malte Schwerhoff
Integrated Semantics of Intermediate-Language-C+Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXTSabine Schmaltz and Andrey Shadrin
Specifying and Verifying the Correctness of Dynamic Software UpdatesChristopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster and Jeffrey S. Foster
A Lightweight Technique for Distributed and Incremental Program VerificationMartin Brain and Florian Schanda
A Comparison of Intermediate Verification Languages: Boogie and Sireum/PilarLoren Segal and Patrice Chalin
Symbolic Execution Enhanced System TestingMisty Davies, Corina Pasareanu and Vishwanath Raman
Isabelle/Circus : a Process Specification and Verification EnvironmentAbderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IRFlorian Merz, Stephan Falke and Carsten Sinz
Verification of TLB Virtualization Implemented in CEyad Alkassar, Ernie Cohen, Mikhail Kovalev and Wolfgang J. Paul
Formalization and Analysis of Real-Time Requirements: a Feasibility Study at BOSCHAmalinda Post and Jochen Hoenicke
The Location Linking Concept: A Basis for Verification of Code Using PointersGregory Kulczycki, Hampton Smith, Heather Harton, Murali Sitaraman, William Ogden and Joseph Hollingsworth
Verifying implementations of security protocols by refinementNadia Polikarpova and Michał Moskal
Deciding Functional Lists with Sublist SetsThomas Wies, Marco Muniz and Viktor Kuncak

We received a total of 54 submissions, of which 20 were accepted.