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