Abstract is missing.
- Variations on SafetyOrna Kupferman. 1-14 [doi]
- Decision Procedures for Flat Array PropertiesFrancesco Alberti, Silvio Ghilardi, Natasha Sharygina. 15-30 [doi]
- SATMC: A SAT-Based Model Checker for Security-Critical SystemsAlessandro Armando, Roberto Carbone, Luca Compagna. 31-45 [doi]
- IC3 Modulo Theories via Implicit Predicate AbstractionAlessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. 46-61 [doi]
- SMT-Based Verification of Software Countermeasures against Side-Channel AttacksHassan Eldib, Chao Wang, Patrick Schaumont. 62-77 [doi]
- Detecting Unrealizable Specifications of Distributed SystemsBernd Finkbeiner, Leander Tentrup. 78-92 [doi]
- Synthesizing Safe Bit-Precise InvariantsArie Gurfinkel, Anton Belov, Joao Marques-Silva. 93-108 [doi]
- PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust EvidenceMichael Huth, Jim Huan-Pu Kuo. 109-123 [doi]
- GRASShopper - Complete Heap Verification with Mixed SpecificationsRuzica Piskac, Thomas Wies, Damien Zufferey. 124-139 [doi]
- Alternating Runtime and Size Complexity Analysis of Integer ProgramsMarc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl. 140-155 [doi]
- Proving Nontermination via SafetyHong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn. 156-171 [doi]
- Ranking Templates for Linear LoopsJan Leike, Matthias Heizmann. 172-186 [doi]
- FDR3 - A Modern Refinement Checker for CSPThomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, A. W. Roscoe. 187-201 [doi]
- Concurrent Depth-First Search AlgorithmsGavin Lowe. 202-216 [doi]
- Basic Problems in Multi-View ModelingJan Reineke, Stavros Tripakis. 217-232 [doi]
- GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUsAnton Wijs, Dragan Bosnacki. 233-247 [doi]
- Forward Reachability Computation for Autonomous Max-Plus-Linear SystemsDieky Adzkiya, Bart De Schutter, Alessandro Abate. 248-262 [doi]
- Compositional Invariant Generation for Timed SystemsLacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz. 263-278 [doi]
- Characterizing Algebraic Invariants by Differential Radical InvariantsKhalil Ghorbal, André Platzer. 279-294 [doi]
- Quasi-Equal Clock Reduction: More Networks, More QueriesChristian Herrera, Bernd Westphal, Andreas Podelski. 295-309 [doi]
- Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed AutomataTing Wang, Jun Sun 0001, Yang Liu, Xinyu Wang, Shanping Li. 310-325 [doi]
- Formal Design of Fault Detection and Identification Components Using Temporal Epistemic LogicMarco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta. 326-340 [doi]
- Monitoring Modulo TheoriesNormann Decker, Martin Leucker, Daniel Thoma. 341-356 [doi]
- Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time SystemsThomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann. 357-372 [doi]
- Status Report on Software Verification - (Competition Summary SV-COMP 2014)Dirk Beyer. 373-388 [doi]
- CBMC - C Bounded Model Checker - (Competition Contribution)Daniel Kroening, Michael Tautschnig. 389-391 [doi]
- CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution)Stefan Löwe, Mikhail Mandrykin, Philipp Wendler. 392-394 [doi]
- CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution)Petr Müller, Tomás Vojnar. 395-397 [doi]
- Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution)Omar Inverso, Ermenegildo Tomasco, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 398-401 [doi]
- MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution)Ermenegildo Tomasco, Omar Inverso, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 402-404 [doi]
- ESBMC 1.22 - (Competition Contribution)Jeremy Morse, Mikhail Ramalho, Lucas Cordeiro, Denis Nicole, Bernd Fischer 0002. 405-407 [doi]
- FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution)Arie Gurfinkel, Anton Belov. 408-411 [doi]
- Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution)Kamil Dudka, Petr Peringer, Tomás Vojnar. 412-414 [doi]
- Symbiotic 2: More Precise Slicing - (Competition Contribution)Jiri Slaby, Jan Strejcek. 415-417 [doi]
- Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution)Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski. 418-420 [doi]
- Ultimate Kojak - (Competition Contribution)Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski. 421-423 [doi]
- Discounting in LTLShaull Almagor, Udi Boker, Orna Kupferman. 424-439 [doi]
- Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing AutomataAla-Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg. 440-454 [doi]
- Symbolic Synthesis for Epistemic Specifications with Observational SemanticsXiaowei Huang, Ron van der Meyden. 455-469 [doi]
- Synthesis for Human-in-the-Loop Control SystemsWenchao Li, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia. 470-484 [doi]
- Learning Regular Languages over Large AlphabetsOded Maler, Irini-Eleftheria Mens. 485-499 [doi]
- Verification of Concurrent Quantum Protocols by Equivalence CheckingEbrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan. 500-514 [doi]
- Computing Conditional Probabilities in Markovian Models EfficientlyChristel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker. 515-530 [doi]
- Permissive Controller Synthesis for Probabilistic SystemsKlaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma. 531-546 [doi]
- Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic InvarianceSadegh Esmaeil Zadeh Soudjani, Alessandro Abate. 547-561 [doi]
- SACO: Static Analyzer for Concurrent ObjectsElvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Román-Díez. 562-567 [doi]
- VeriMAP: A Tool for Verifying Programs through TransformationsEmanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti. 568-574 [doi]
- CIF 3: Model-Based Engineering of Supervisory ControllersD. A. van Beek, Wan Fokkink, D. Hendriks, A. Hofkamp, Jasen Markovski, J. M. van de Mortel-Fronczak, Michel A. Reniers. 575-580 [doi]
- EDD: A Declarative Debugger for Sequential Erlang ProgramsRafael Caballero, Enrique Martin-Martin, Adrián Riesco, Salvador Tamarit. 581-586 [doi]
- APTE: An Algorithm for Proving Trace EquivalenceVincent Cheval. 587-592 [doi]
- The Modest Toolset: An Integrated Environment for Quantitative Modelling and VerificationArnd Hartmanns, Holger Hermanns. 593-598 [doi]
- Bounds2: A Tool for Compositional Multi-parametrised VerificationAntti Siirtola. 599-604 [doi]
- On the Correctness of a Branch Displacement AlgorithmJaap Boender, Claudio Sacerdoti Coen. 605-619 [doi]
- Analyzing the Next Generation Airborne Collision Avoidance SystemChristian von Essen, Dimitra Giannakopoulou. 620-635 [doi]
- Environment-Model Based Testing of Control Systems: Case StudiesErwan Jahier, Simplice Djoko Djoko, Chaouki Maiza, Eric Lafont. 636-650 [doi]