Accepted Papers
- John Derrick, Graeme Smith, Brijesh Dongol, and Lindsay Groves
Using coarse-grained abstractions to verify linearizability on TSO architectures
- Eitan Marcus, Avi Ziv, and Yoav Katz
Enhancing Scenario Quality Using Quasi-Events
- Georges Morbé, Christoph Scholl, Bernd Becker, and Christian Miller
Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems
- Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller
DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification
- Gadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, and Dan Rasin
Generating Linear Invariants for Model Checking
- Georg Hofferek and Ashutosh Gupta
TheTool - A Controller Synthesis Tool Using Uninterpreted Functions
- Rajeev Alur, Milo Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa
Synthesizing Finite-state Protocols from Scenarios and Requirements
- Robert Koenighofer, Ronald Toegl, and Roderick Bloem
Automatic Error Localization for Software Using Deductive Verification
- Christoph Gladisch, Daniel Grunwald, Tianhai Liu, Mana Taghdiri, and Shmuel Tyszberowicz
Generating JML Specifications from Alloy Expressions
- Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump
Assume-Guarantee Abstraction Refinement Meets Hybrid Systems
- Oleg Travkin and Heike Wehrheim
Handling TSO in Mechanized Linearizability Proofs
- Eugene Goldberg and Panagiotis Manolios
Partial Quantifier Elimination
- Mikhail Lukin, Maxim Buzdalov, and Anatoly Shalyto
Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study
- Duc-Hiep Chu and Joxan Jaffar
A Framework to Synergize Partial Order Reduction with State Interpolation
- Roderick Bloem, Sharad Malik, Matthias Schlaipfer, and Georg Weissenbacher
Reduction of Resolution Refutations and Interpolants via Subsumption
- Jeroen Meijer, Gijs Kant, Stefan Blom, and Jaco van de Pol
Read, Write, and Copy Dependencies for Symbolic Model Checking
- Angelo Gargantini and Paolo Vavassori
Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams
- Oliver Schwarz and Mads Dam
Formal Verification of Secure User Mode Device Execution with DMA
- Mohammad Reza Shoaei, Laura Kovacs, and Bengt Lennartson
Supervisory Control of Discrete-Event Systems via IC3
- Alfons Laarman and Anton Wijs
Partial Order Reduction for Multi-Core LTL Model Checking
- Tianhai Liu, Mateus Borges, Marcelo D'Amorim, and Mana Taghdiri
A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution
Keynote Speakers
- Prof. Moshe Vardi, Rice University
- Wolfgang Roesner, Fellow, IBM
- Prof. Martin Vechev, ETH Zürich
- Harry Foster, Chief Verification Scientist, Mentor Graphics
- Ziv Binyamini, Corporate VP & CTO, System and Software Solutions, Cadence
