Abstract is missing.
- Moving Fast with Software VerificationCristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez. 3-11 [doi]
- Developing Verified Software Using LeonViktor Kuncak. 12-15 [doi]
- Timely Rollback: Specification and VerificationMartín Abadi, Michael Isard. 19-34 [doi]
- Sum of Abstract DomainsGianluca Amato, Simone Di Nardo Di Maio, Francesca Scozzari. 35-49 [doi]
- Reachability Preservation Based Parameter Synthesis for Timed AutomataÉtienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun. 50-65 [doi]
- Compositional Verification of Parameterised Timed SystemsLacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz. 66-81 [doi]
- Requirements Analysis of a Quad-Redundant Flight Control SystemJohn Backes, Darren D. Cofer, Steven P. Miller, Michael W. Whalen. 82-96 [doi]
- Partial Order Reduction and Symmetry with Multiple RepresentativesDragan Bosnacki, Mark Scheffer. 97-111 [doi]
- Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid NetworksAlice Dal Corso, Damiano Macedonio, Massimo Merro. 112-126 [doi]
- Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid SystemsTommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh. 127-142 [doi]
- First-Order Transitive Closure Axiomatization via Iterative Invariant InjectionsAboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda. 143-157 [doi]
- Reachability Analysis Using Extremal RatesAndrew N. Fisher, Chris J. Myers, Peng Li. 158-172 [doi]
- Towards Realizability Checking of Contracts Using TheoriesAndrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer. 173-187 [doi]
- Practical Partial Order Reduction for CSPThomas Gibson-Robinson, Henri Hansen, A. William Roscoe, Xu Wang. 188-203 [doi]
- A Little Language for TestingAlex Groce, Jervis Pinto. 204-218 [doi]
- Detecting MPI Zero Buffer Incompatibility by SMT EncodingYu Huang, Eric Mercer. 219-233 [doi]
- A Falsification View of Success TypingRobert Jakob, Peter Thiemann. 234-247 [doi]
- Verified ROS-Based Deployment of Platform-Independent Control SystemsWenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee. 248-262 [doi]
- A Rigorous Approach to Combining Use Case Modelling and Accident ScenariosRajiv Murali, Andrew Ireland, Gudmund Grov. 263-278 [doi]
- Are We There Yet? Determining the Adequacy of Formalized Requirements and Test SuitesAnitha Murugesan, Michael W. Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Per Erik Heimdahl, Dongjiang You. 279-294 [doi]
- A Greedy Approach for the Efficient Repair of Stochastic ModelsShashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. 295-309 [doi]
- Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit VerificationYan Peng, Mark R. Greenstreet. 310-326 [doi]
- Conflict-Directed Graph CoverageDaniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanovic, Philipp Rümmer, Thomas Wies. 327-342 [doi]
- Shape Analysis with ConnectorsHolger Siegel, Axel Simon. 343-358 [doi]
- Automated Conflict-Free Concurrent Implementation of Timed Component-Based ModelsAhlem Triki, Borzoo Bonakdarpour, Jacques Combaz, Saddek Bensalem. 359-374 [doi]
- Formal API Specification of the PikeOS Separation KernelFreek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan 0004, Burkhart Wolff, Yakoub Nemouchi. 375-389 [doi]
- Data Model BugsIvan Bocic, Tevfik Bultan. 393-399 [doi]
- Predicting and Witnessing Data Races Using CSPLuis M. Carril, Walter F. Tichy. 400-407 [doi]
- A Benchmark Suite for Hybrid Systems Reachability AnalysisXin Chen 0002, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski. 408-414 [doi]
- Generalizing a Mathematical Analysis Library in Isabelle/HOLJesús Aransay, Jose Divasón. 415-421 [doi]
- A Tool for Intersecting Context-Free Grammars and Its ApplicationsGraeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey. 422-428 [doi]
- UFIT: A Tool for Modeling Faults in UPPAAL Timed AutomataReza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni. 429-435 [doi]
- Blocked Literals Are UniversalMarijn Heule, Martina Seidl, Armin Biere. 436-442 [doi]
- Practical Formal Verification of Domain-Specific Language ApplicationsGreg Eakman, Howard Reubenstein, Tom Hawkins, Mitesh Jain, Panagiotis Manolios. 443-449 [doi]
- Reporting Races in Dynamic Partial Order ReductionOlli Saarikivi, Keijo Heljanko. 450-456 [doi]