Abstract is missing.
- On-the-Fly Exact Computation of Bisimilarity DistancesGiorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare. 1-15 [doi]
- The Quest for Minimal Quotients for Probabilistic AutomataChristian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang 0001. 16-31 [doi]
- LTL Model Checking of Interval Markov ChainsMichael Benedikt, Rastislav Lenhardt, James Worrell. 32-46 [doi]
- Ramsey vs. Lexicographic Termination ProvingByron Cook, Abigail See, Florian Zuleger. 47-61 [doi]
- Structural Counter AbstractionKshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey. 62-77 [doi]
- Extending Quantifier Elimination to Linear Inequalities on Bit-VectorsAjith K. John, Supratik Chakraborty. 78-92 [doi]
- The MathSAT5 SMT SolverAlessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani. 93-107 [doi]
- Formula Preprocessing in MUS ExtractionAnton Belov, Matti Järvisalo, João Marques-Silva. 108-123 [doi]
- Proof Tree Preserving InterpolationJürgen Christ, Jochen Hoenicke, Alexander Nutz. 124-138 [doi]
- Asynchronous Multi-core Incremental SAT SolvingSiert Wieringa, Keijo Heljanko. 139-153 [doi]
- Model-Checking Iterated GamesChung-Hao Huang, Sven Schewe, Farn Wang. 154-168 [doi]
- Synthesis from LTL Specifications with Mean-Payoff ObjectivesAaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin. 169-184 [doi]
- PRISM-games: A Model Checker for Stochastic Multi-Player GamesTaolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. 185-191 [doi]
- PIC2LNT: Model Transformation for Model Checking an Applied Pi-CalculusRadu Mateescu, Gwen Salaün. 192-198 [doi]
- An Overview of the mCRL2 Toolset and Its Recent AdvancesSjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, Tim A. C. Willemse. 199-213 [doi]
- Analysis of Boolean ProgramsPatrice Godefroid, Mihalis Yannakakis. 214-229 [doi]
- Weighted Pushdown Systems with Indexed Weight DomainsYasuhiko Minamide. 230-244 [doi]
- Underapproximation of Procedure Summaries for Integer ProgramsPierre Ganty, Radu Iosif, Filip Konecný. 245-259 [doi]
- Runtime Verification Based on Register AutomataRadu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos. 260-276 [doi]
- Unbounded Model-Checking with Interpolation for Regular Language ConstraintsGraeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte. 277-291 [doi]
- eVolCheck: Incremental Upgrade Checker for CGrigory Fedyukovich, Ondrej Sery, Natasha Sharygina. 292-307 [doi]
- Intertwined Forward-Backward Reachability Analysis Using InterpolantsYakir Vizel, Orna Grumberg, Sharon Shoham. 308-323 [doi]
- An Integrated Specification and Verification Technique for Highly Concurrent Data StructuresParosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, Ahmed Rezine. 324-338 [doi]
- A Verification-Based Approach to Memory Fence Insertion in PSO Memory SystemsAlexander Linden, Pierre Wolper. 339-353 [doi]
- Identifying Dynamic Data Structures by Learning Evolving Patterns in MemoryDavid H. White, Gerald Lüttgen. 354-369 [doi]
- Synthesis of Circular Compositional Program Proofs via AbductionBoyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv. 370-384 [doi]
- As Soon as Probable: Optimal Scheduling under Stochastic UncertaintyJean-Francois Kempf, Marius Bozga, Oded Maler. 385-400 [doi]
- Integer Parameter Synthesis for Timed AutomataAleksandra Jovanovic, Didier Lime, Olivier H. Roux. 401-415 [doi]
- LTL Model-Checking for Malware DetectionFu Song, Tayssir Touili. 416-431 [doi]
- Policy Analysis for Self-administrated Role-Based Access ControlAnna Lisa Ferrara, P. Madhusudan, Gennaro Parlato. 432-447 [doi]
- Model Checking Agent Knowledge in Dynamic Access Control PoliciesMasoud Koleini, Eike Ritter, Mark Ryan. 448-462 [doi]
- Automatic Testing of Real-Time Graphics SystemsRobert Nagy, Gerardo Schneider, Aram Timofeitchik. 463-477 [doi]
- Equivalence Checking of Quantum ProtocolsEbrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan. 478-492 [doi]
- Encoding Monomorphic and Polymorphic TypesJasmin Christian Blanchette, Sascha Böhme, Andrei Popescu 0001, Nicholas Smallbone. 493-507 [doi]
- Deriving Probability Density Functions from Probabilistic Functional ProgramsSooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo. 508-522 [doi]
- Polyglot: Systematic Analysis for Multiple Statechart FormalismsDaniel Balasubramanian, Corina S. Pasareanu, Gabor Karsai, Michael R. Lowry. 523-529 [doi]
- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSOParosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine. 530-536 [doi]
- BULL: A Library for Learning Algorithms of Boolean FunctionsYu-Fang Chen, Bow-Yaw Wang. 537-542 [doi]
- AppGuard - Enforcing User Requirements on Android AppsMichael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei, Philipp von Styp-Rekowsky. 543-548 [doi]
- Model Checking Database ApplicationsMilos Gligoric, Rupak Majumdar. 549-564 [doi]
- Efficient Property Preservation Checking of Model RefinementsAnton Wijs, Luc Engelen. 565-579 [doi]
- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model CheckingEtienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. 580-593 [doi]
- Second Competition on Software Verification - (Summary of SV-COMP 2013)Dirk Beyer. 594-609 [doi]
- CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution)Stefan Löwe. 610-612 [doi]
- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution) Philipp Wendler. 613-615 [doi]
- CSeq: A Sequentialization Tool for C - (Competition Contribution)Bernd Fischer 0002, Omar Inverso, Gennaro Parlato. 616-618 [doi]
- Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution)Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer 0002. 619-622 [doi]
- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution)Stephan Falke, Florian Merz, Carsten Sinz. 623-626 [doi]
- Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution)Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar. 627-629 [doi]
- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution)Jiri Slaby, Jan Strejcek, Marek Trtík. 630-632 [doi]
- Threader: A Verifier for Multi-threaded Programs - (Competition Contribution)Corneliu Popeea, Andrey Rybalchenko. 633-636 [doi]
- UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution)Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik. 637-640 [doi]
- Ultimate Automizer with SMTInterpol - (Competition Contribution)Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski. 641-643 [doi]