Abstract is missing.
- Reuse of Verification Results - Conditional Model Checking, Precision Reuse, and Verification WitnessesDirk Beyer, Philipp Wendler. 1-17 [doi]
- Proving Properties of Concurrent Programs - (Extended Abstract)Gerard J. Holzmann. 18-23 [doi]
- Verifying a Quantitative Relaxation of Linearizability via RefinementKiran Adhikari, James Street, Chao Wang, Yang Liu, Shao Jie Zhang. 24-42 [doi]
- A Map-Reduce Parallel Approach to Automatic Synthesis of Control SoftwareVadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci. 43-60 [doi]
- On-the-Fly Control Software SynthesisVadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci. 61-80 [doi]
- Compositional Approach to Suspension and Other Improvements to LTL TranslationTomás Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek. 81-98 [doi]
- Regression Verification Using Impact SummariesJohn Backes, Suzette Person, Neha Rungta, Oksana Tkachuk. 99-116 [doi]
- Abstraction-Based Guided Search for Hybrid SystemsSergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle. 117-134 [doi]
- Probabilistic Verification of Coordinated Multi-robot MissionsSagar Chaki, Joseph Andrew Giampapa. 135-153 [doi]
- Synthesizing Controllers for Automation Tasks with Performance GuaranteesChih-Hong Cheng, Michael Geisinger, Christian Buckl. 154-159 [doi]
- Specification and Validation of Link Reversal Routing via Graph TransformationsGiorgio Delzanno, Riccardo Traverso. 160-177 [doi]
- Local Model Checking of Weighted CTL with Upper-Bound ConstraintsJonas Finnemann Jensen, Kim Guldstrand Larsen, Jirí Srba, Lars Kaerlund Oestergaard. 178-195 [doi]
- COMPLeTe - A COMmunication Protocol vaLidation ToolchainSven Gröning, Christopher Rosas, Christian Wietfeld. 196-208 [doi]
- Towards Modeling and Model Checking Fault-Tolerant Distributed AlgorithmsAnnu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder. 209-226 [doi]
- Guard-Based Partial-Order ReductionAlfons Laarman, Elwin Pater, Jaco van de Pol, Michael Weber 0002. 227-245 [doi]
- On the Synergy of Probabilistic Causality Computation and Causality CheckingFlorian Leitner-Fischer, Stefan Leue. 246-263 [doi]
- Mining Sequential Patterns to Explain Concurrent CounterexamplesStefan Leue, Mitra Tabaei Befrouei. 264-281 [doi]
- Automatic Equivalence Checking of UF+IA ProgramsNuno P. Lopes, José Monteiro. 282-300 [doi]
- Expression Reduction from Programs in a Symbolic Binary ExecutorAnthony Romano, Dawson Engler. 301-319 [doi]
- Model Checking Unbounded Concurrent ListsDivjyot Sethi, Muralidhar Talupur, Sharad Malik. 320-340 [doi]
- Property-Driven Benchmark GenerationBernhard Steffen, Malte Isberner, Stefan Naujokat, Tiziana Margaria, Maren Geske. 341-357 [doi]
- Error-Completion in Interface TheoriesStavros Tripakis, Christos Stergiou, Manfred Broy, Edward A. Lee. 358-375 [doi]