Abstract is missing.
- Quantitative Models for a Not So Dumb GridHolger Hermanns. 1 [doi]
- History-Aware Data Structure Repair Using SATRazieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, Kathryn S. McKinley. 2-17 [doi]
- The Guardol Language and Verification SystemDavid S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham. 18-32 [doi]
- A Bit Too Precise? Bounded Verification of Quantized Digital FiltersArlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang. 33-47 [doi]
- Numeric Bounds Analysis with Conflict-Driven LearningVijay D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig. 48-63 [doi]
- Ramsey-Based Analysis of Parity AutomataOliver Friedmann, Martin Lange. 64-78 [doi]
- VATA: A Library for Efficient Manipulation of Non-deterministic Tree AutomataOndrej Lengál, Jirí Simácek, Tomás Vojnar. 79-94 [doi]
- LTL to Büchi Automata Translation: Fast and More DeterministicTomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek. 95-109 [doi]
- Pushdown Model Checking for Malware DetectionFu Song, Tayssir Touili. 110-125 [doi]
- Aspect-Oriented Runtime Monitor CertificationKevin W. Hamlen, Micah Jones, Meera Sridhar. 126-140 [doi]
- Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation SystemsFrédéric Lang, Radu Mateescu. 141-156 [doi]
- From Under-Approximations to Over-Approximations and BackAws Albarghouthi, Arie Gurfinkel, Marsha Chechik. 157-172 [doi]
- Automated Analysis of AODV Using UPPAALAnsgar Fehnker, Rob J. van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan. 173-187 [doi]
- Modeling and Verification of a Dual Chamber Implantable PacemakerZhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam. 188-203 [doi]
- Counter-Example Guided Fence Insertion under TSOParosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine. 204-219 [doi]
- Java Memory Model-Aware Model CheckingHuafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders. 220-236 [doi]
- Compositional Termination Proofs for Multi-threaded ProgramsCorneliu Popeea, Andrey Rybalchenko. 237-251 [doi]
- Deciding Conditional TerminationMarius Bozga, Radu Iosif, Filip Konecný. 252-266 [doi]
- The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented ArchitecturesAlessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta, Alberto Calvi, Alessandro Cappai, Roberto Carbone, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Gabriel Erzse, Simone Frau, Marius Minea, Sebastian Mödersheim, David von Oheimb, Giancarlo Pellegrino, Serena Elisa Ponta, Marco Rocchetto, Michaël Rusinowitch, Mohammad Torabi Dashti, Mathieu Turuani, Luca Viganò. 267-282 [doi]
- Reduction-Based Formal Analysis of BGP InstancesAnduo Wang, Carolyn L. Talcott, Alexander J. T. Gurney, Boon Thau Loo, Andre Scedrov. 283-298 [doi]
- Minimal Critical Subsystems for Discrete-Time Markov ModelsRalf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen. 299-314 [doi]
- Automatic Verification of Competitive Stochastic SystemsTaolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. 315-330 [doi]
- Coupling and Importance Sampling for Statistical Model CheckingBenoît Barbot, Serge Haddad, Claudine Picaronny. 331-346 [doi]
- Verifying pCTL Model CheckingJohannes Hölzl, Tobias Nipkow. 347-361 [doi]
- Parameterized SynthesisSwen Jacobs, Roderick Bloem. 362-376 [doi]
- QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and VerificationHu-Hsi Yeh, Cheng-Yin Wu, Chung-Yang (Ric) Huang. 377-391 [doi]
- Template-Based Controller Synthesis for Timed SystemsBernd Finkbeiner, Hans-Jörg Peter. 392-406 [doi]
- Zeno: An Automated Prover for Properties of Recursive Data StructuresWilliam Sonnex, Sophia Drossopoulou, Susan Eisenbach. 407-421 [doi]
- A Proof Assistant for Alloy SpecificationsMattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri. 422-436 [doi]
- Reachability under Contextual LockingRohit Chadha, P. Madhusudan, Mahesh Viswanathan. 437-450 [doi]
- Bounded Phase Analysis of Message-Passing ProgramsAhmed Bouajjani, Michael Emmi. 451-465 [doi]
- Demonstrating Learning of Register AutomataMaik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel, Bengt Jonsson. 466-471 [doi]
- Symbolic Automata: The ToolkitMargus Veanes, Nikolaj Bjørner. 472-477 [doi]
- McScM: A General Framework for the Verification of Communicating MachinesAlexander Heußner, Tristan Le Gall, Grégoire Sutre. 478-484 [doi]
- SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic SpecificationsLuís Caires, Hugo Torres Vieira. 485-491 [doi]
- TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri NetsAlexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jirí Srba. 492-497 [doi]
- A Platform for High Performance Statistical Model Checking - PLASMACyrille Jégourel, Axel Legay, Sean Sedwards. 498-503 [doi]
- Competition on Software Verification - (SV-COMP)Dirk Beyer. 504-524 [doi]
- Predicate Analysis with BLAST 2.7 - (Competition Contribution)Pavel Shved, Mikhail Mandrykin, Vadim Mutilin. 525-527 [doi]
- CPAchecker with Adjustable Predicate Analysis - (Competition Contribution)Stefan Löwe, Philipp Wendler. 528-530 [doi]
- Block Abstraction Memoization for CPAchecker - (Competition Contribution)Daniel Wonisch. 531-533 [doi]
- Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution)Lucas Cordeiro, Jeremy Morse, Denis Nicole, Bernd Fischer 0002. 534-537 [doi]
- Proving Reachability Using FShell - (Competition Contribution)Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith. 538-541 [doi]
- LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution)Carsten Sinz, Florian Merz, Stephan Falke. 542-544 [doi]
- Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution)Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar. 545-548 [doi]
- HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution)Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko. 549-551 [doi]
- satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution)Gérard Basler, Alastair F. Donaldson, Alexander Kaiser 0001, Daniel Kroening, Michael Tautschnig, Thomas Wahl. 552-555 [doi]
- Wolverine: Battling Bugs with Interpolants - (Competition Contribution)Georg Weissenbacher, Daniel Kroening, Sharad Malik. 556-558 [doi]