| 2013 | A Fully Verified Executable LTL Model Checker. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | A Scalable and Nearly Uniform Generator of SAT Witnesses. Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2013 | A Tool for Estimating Information Leakage. Tom Chothia, Yusuke Kawamoto, Chris Novakovic |
| 2013 | Abstraction Based Model-Checking of Stability of Hybrid Systems. Pavithra Prabhakar, Miriam Garcia Soto |
| 2013 | Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský |
| 2013 | Automatic Abstraction in SMT-Based Unbounded Software Model Checking. Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke |
| 2013 | Automatic Generation of Quality Specifications. Shaull Almagor, Guy Avni, Orna Kupferman |
| 2013 | Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger |
| 2013 | Automating Separation Logic Using SMT. Ruzica Piskac, Thomas Wies, Damien Zufferey |
| 2013 | Beautiful Interpolants. Aws Albarghouthi, Kenneth L. McMillan |
| 2013 | Better Termination Proving through Cooperation. Marc Brockschmidt, Byron Cook, Carsten Fuhs |
| 2013 | CacBDD: A BDD Package with Dynamic Cache Management. Guanfeng Lv, Kaile Su, Yanyan Xu |
| 2013 | Combining Relational Learning with SMT Solvers Using CEGAR. Arun Tejasvi Chaganty, Akash Lal, Aditya V. Nori, Sriram K. Rajamani |
| 2013 | Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings Natasha Sharygina, Helmut Veith |
| 2013 | DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, Jirí Weiser |
| 2013 | Disjunctive Interpolants for Horn-Clause Verification. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak |
| 2013 | Distributed Explicit State Model Checking of Deadlock Freedom. Brad D. Bingham, Jesse D. Bingham, John Erickson, Mark R. Greenstreet |
| 2013 | Duet: Static Analysis for Unbounded Parallelism. Azadeh Farzan, Zachary Kincaid |
| 2013 | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | Efficient Generation of Small Interpolants in CNF. Yakir Vizel, Vadim Ryvchin, Alexander Nadel |
| 2013 | Efficient Robust Monitoring for STL. Alexandre Donzé, Thomas Ferrère, Oded Maler |
| 2013 | Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
| 2013 | Equivalence of Extended Symbolic Finite Transducers. Loris D'Antoni, Margus Veanes |
| 2013 | Explain: A Tool for Performing Abductive Inference. Isil Dillig, Thomas Dillig |
| 2013 | Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. Lubos Brim, Milan Ceska, Sven Drazan, David Safránek |
| 2013 | Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems. Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung, Ming Gu |
| 2013 | Faster Algorithms for Markov Decision Processes with Low Treewidth. Krishnendu Chatterjee, Jakub Lacki |
| 2013 | Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. Adi Sosnovich, Orna Grumberg, Gabi Nakibly |
| 2013 | Finite Model Finding in SMT. Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic |
| 2013 | First-Order Theorem Proving and Vampire. Laura Kovács, Andrei Voronkov |
| 2013 | Flow*: An Analyzer for Non-linear Hybrid Systems. Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan |
| 2013 | Formal Verification of Hardware Synthesis. Thomas Braibant, Adam Chlipala |
| 2013 | Fully Automated Shape Analysis Based on Forest Automata. Lukás Holík, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar |
| 2013 | GOAL for Games, Omega-Automata, and Logics. Ming-Hsien Tsai, Yih-Kuen Tsay, Yu-Shiang Hwang |
| 2013 | Generating Non-linear Interpolants by Semidefinite Programming. Liyun Dai, Bican Xia, Naijun Zhan |
| 2013 | ILP Modulo Theories. Panagiotis Manolios, Vasilis Papavasileiou |
| 2013 | Importance Splitting for Statistical Model Checking Rare Properties. Cyrille Jégourel, Axel Legay, Sean Sedwards |
| 2013 | Incremental, Inductive Coverability. Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac |
| 2013 | JBernstein: A Validity Checker for Generalized Polynomial Constraints. Chih-Hong Cheng, Harald Ruess, Natarajan Shankar |
| 2013 | Lazy Abstractions for Timed Automata. Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz |
| 2013 | Learning Universally Quantified Invariants of Linear Data Structures. Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider |
| 2013 | Lengths May Break Privacy - Or How to Check for Equivalences with Length. Vincent Cheval, Véronique Cortier, Antoine Plet |
| 2013 | Minimal Sets over Monotone Predicates in Boolean Formulae. João Marques-Silva, Mikolás Janota, Anton Belov |
| 2013 | Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Qinsi Wang |
| 2013 | Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction. Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol |
| 2013 | Multi-solver Support in Symbolic Execution. Hristina Palikareva, Cristian Cadar |
| 2013 | PARTY Parameterized Synthesis of Token Rings. Ayrat Khalimov, Swen Jacobs, Roderick Bloem |
| 2013 | PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games. Romain Brenguier |
| 2013 | PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. Étienne André, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin |
| 2013 | Parameterized Verification of Asynchronous Shared-Memory Systems. Javier Esparza, Pierre Ganty, Rupak Majumdar |
| 2013 | Partial Orders for Efficient Bounded Model Checking of Concurrent Software. Jade Alglave, Daniel Kroening, Michael Tautschnig |
| 2013 | Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
| 2013 | Probabilistic Program Analysis with Martingales. Aleksandar Chakarov, Sriram Sankaranarayanan |
| 2013 | Program Repair without Regret. Christian von Essen, Barbara Jobstmann |
| 2013 | Programs from Proofs - A PCC Alternative. Daniel Wonisch, Alexander Schremmer, Heike Wehrheim |
| 2013 | Proving Termination Starting from the End. Pierre Ganty, Samir Genaim |
| 2013 | QUAIL: A Quantitative Security Analyzer for Imperative Code. Fabrizio Biondi, Axel Legay, Louis-Marie Traonouez, Andrzej Wasowski |
| 2013 | Recursive Program Synthesis. Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid |
| 2013 | Relative Equivalence in the Presence of Ambiguity. Oshri Adler, Cindy Eisner, Tatyana Veksler |
| 2013 | SVA and PSL Local Variables - A Practical Approach. Roy Armoni, Dana Fisman, Naiyong Jin |
| 2013 | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson |
| 2013 | Shrinktech: A Tool for the Robustness Analysis of Timed Automata. Ocan Sankur |
| 2013 | Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries. Richard Uhler, Nirav Dave |
| 2013 | Software Model Checking for People Who Love Automata. Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2013 | Solving Existentially Quantified Horn Clauses. Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko |
| 2013 | System Level Formal Verification via Model Checking Driven Simulation. Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli, Enrico Tronci |
| 2013 | TTP: Tool for Tumor Progression. Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee, Martin A. Nowak |
| 2013 | The TAMARIN Prover for the Symbolic Analysis of Security Protocols. Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin |
| 2013 | Towards Distributed Software Model-Checking Using Decision Diagrams. Maximilien Colange, Souheib Baarir, Fabrice Kordon, Yann Thierry-Mieg |
| 2013 | Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks. Loïc Paulevé, Geoffroy Andrieux, Heinz Koeppl |
| 2013 | Under-Approximating Loops in C Programs for Fast Counterexample Detection. Daniel Kroening, Matt Lewis, Georg Weissenbacher |
| 2013 | Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata. Alistair Stewart, Kousha Etessami, Mihalis Yannakakis |
| 2013 | Validating Library Usage Interactively. William R. Harris, Guoliang Jin, Shan Lu, Somesh Jha |