| 2013 | TTP: Tool for Tumor Progression. | Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee, Martin A. Nowak |
| 2013 | Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. | Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
| 2013 | Abstraction Based Model-Checking of Stability of Hybrid Systems. | Pavithra Prabhakar, Miriam Garcia Soto |
| 2013 | Automating Separation Logic Using SMT. | Ruzica Piskac, Thomas Wies, Damien Zufferey |
| 2013 | Program Transformation for Program Verification. | Alberto Pettorossi, Maurizio Proietti |
| 2013 | Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks. | Loc Paulev, Geoffroy Andrieux, Heinz Koeppl |
| 2013 | Multi-solver Support in Symbolic Execution. | Hristina Palikareva, Cristian Cadar |
| 2013 | Ping-Pong Protocols as Prefix Grammars and Turchin Relation. | Antonina Nepeivoda |
| 2013 | Transforming Event B Models into Verified C# Implementations. | Dominique Mry, Rosemary Monahan |
| 2013 | The TAMARIN Prover for the Symbolic Analysis of Security Protocols. | Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin |
| 2013 | Minimal Sets over Monotone Predicates in Boolean Formulae. | Joo Marques-Silva, Mikols Janota, Anton Belov |
| 2013 | ILP Modulo Theories. | Panagiotis Manolios, Vasilis Papavasileiou |
| 2013 | System Level Formal Verification via Model Checking Driven Simulation. | Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli, Enrico Tronci |
| 2013 | CacBDD: A BDD Package with Dynamic Cache Management. | Guanfeng Lv, Kaile Su, Yanyan Xu |
| 2013 | Acceleration For Presburger Petri Nets. | Jrme Leroux |
| 2013 | Multi-core Emptiness Checking of Timed Bchi Automata Using Inclusion Abstraction. | Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol |
| 2013 | Under-Approximating Loops in C Programs for Fast Counterexample Detection. | Daniel Kroening, Matt Lewis, Georg Weissenbacher |
| 2013 | First-Order Theorem Proving and Vampire. | Laura Kovcs, Andrei Voronkov |
| 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 | Automatic Abstraction in SMT-Based Unbounded Software Model Checking. | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke |
| 2013 | Incremental, Inductive Coverability. | Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac |
| 2013 | PARTY Parameterized Synthesis of Token Rings. | Ayrat Khalimov, Swen Jacobs, Roderick Bloem |
| 2013 | Importance Splitting for Statistical Model Checking Rare Properties. | Cyrille Jgourel, Axel Legay, Sean Sedwards |
| 2013 | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | Fully Automated Shape Analysis Based on Forest Automata. | Luks Holk, Ondrej Lengl, Adam Rogalewicz, Jir Simcek, Toms Vojnar |