Abstract is missing.
- Using Coarse-Grained Abstractions to Verify Linearizability on TSO ArchitecturesJohn Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol. 1-16 [doi]
- Enhancing Scenario Quality Using Quasi-EventsYoav Katz, Eitan Marcus, Avi Ziv. 17-29 [doi]
- Combined Bounded and Symbolic Model Checking for Incomplete Timed SystemsGeorges Morbé, Christian Miller, Christoph Scholl, Bernd Becker. 30-47 [doi]
- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional VerificationJuan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller. 48-53 [doi]
- Generating Modulo-2 Linear Invariants for Hardware Model CheckingGadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, Dan Rasin. 54-67 [doi]
- Suraq - A Controller Synthesis Tool Using Uninterpreted FunctionsGeorg Hofferek, Ashutosh Gupta. 68-74 [doi]
- Synthesizing Finite-State Protocols from Scenarios and RequirementsRajeev Alur, Milo M. K. Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, Abhishek Udupa. 75-91 [doi]
- Automatic Error Localization for Software Using Deductive VerificationRobert Könighofer, Ronald Toegl, Roderick Bloem. 92-98 [doi]
- Generating JML Specifications from Alloy ExpressionsDaniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel S. Tyszberowicz. 99-115 [doi]
- Assume-Guarantee Abstraction Refinement Meets Hybrid SystemsSergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina S. Pasareanu, Andreas Podelski, Thomas Strump. 116-131 [doi]
- Handling TSO in Mechanized Linearizability ProofsOleg Travkin, Heike Wehrheim. 132-147 [doi]
- Partial Quantifier EliminationEugene Goldberg, Panagiotis Manolios. 148-164 [doi]
- Formal Verification of 800 Genetically Constructed Automata Programs: A Case StudyMikhail Lukin, Maxim Buzdalov, Anatoly Shalyto. 165-170 [doi]
- A Framework to Synergize Partial Order Reduction with State InterpolationDuc-Hiep Chu, Joxan Jaffar. 171-187 [doi]
- Reduction of Resolution Refutations and Interpolants via SubsumptionRoderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher. 188-203 [doi]
- Read, Write and Copy Dependencies for Symbolic Model CheckingJeroen Meijer, Gijs Kant, Stefan Blom, Jaco van de Pol. 204-219 [doi]
- Efficient Combinatorial Test Generation Based on Multivalued Decision DiagramsAngelo Gargantini, Paolo Vavassori. 220-235 [doi]
- Formal Verification of Secure User Mode Device Execution with DMAOliver Schwarz, Mads Dam. 236-251 [doi]
- Supervisory Control of Discrete-Event Systems via IC3Mohammad Reza Shoaei, Laura Kovács, Bengt Lennartson. 252-266 [doi]
- Partial-Order Reduction for Multi-core LTL Model CheckingAlfons Laarman, Anton Wijs. 267-283 [doi]
- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic ExecutionTianhai Liu, Mateus Araújo, Marcelo d'Amorim, Mana Taghdiri. 284-299 [doi]