| 2013 | An Expressive Framework for Verifying Deadlock Freedom. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2013 | Automated Verification and Strategy Synthesis for Probabilistic Systems. | Marta Z. Kwiatkowska, David Parker |
| 2013 | MoTraS: A Tool for Modal Transition Systems and Their Extensions. | Jan Kretnsk, Salomon Sickert |
| 2013 | Rabinizer 2: Small Deterministic Automata for LTL ∖ GU. | Jan Kretnsk, Rusln Ledesma-Garza |
| 2013 | Improved Upper and Lower Bounds for Bchi Disambiguation. | Hrishikesh Karmarkar, Manas Joglekar, Supratik Chakraborty |
| 2013 | Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games. | Aleksandra Jovanovic, Didier Lime, Olivier H. Roux |
| 2013 | CELL: A Compositional Verification Framework. | Kun Ji, Yang Liu, Shang-Wei Lin, Jun Sun, Jin Song Dong, Truong Khanh Nguyen |
| 2013 | Solving Parity Games on the GPU. | Philipp Hoffmann, Michael Luttenberger |
| 2013 | VCS: A Verifier for Component-Based Systems. | Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng |
| 2013 | Linear Ranking for Linear Lasso Programs. | Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski |
| 2013 | Interpolation Properties and SAT-Based Model Checking. | Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina |
| 2013 | An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2013 | CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. | Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang |
| 2013 | LTL Model Checking with Neco. | Lukasz Fronc, Alexandre Duret-Lutz |
| 2013 | An Automatic Technique for Checking the Simulation of Timed Systems. | Elie Fares, Jean-Paul Bodeveix, Mamoun Filali-Amine, Manuel Garnacho |
| 2013 | Multi-threaded Explicit State Space Exploration with State Reconstruction. | Sami Evangelista, Lars Michael Kristensen, Laure Petrucci |
| 2013 | Kleene Algebras and Semimodules for Energy Problems. | Zoltn sik, Uli Fahrenberg, Axel Legay, Karin Quaas |
| 2013 | Manipulating LTL Formulas Using Spot 1.0. | Alexandre Duret-Lutz |
| 2013 | Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications. | Ramiro Demasi, Pablo F. Castro, T. S. E. Maibaum, Nazareno Aguirre |
| 2013 | SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads. | Alessandro Cimatti |
| 2013 | Control Flow Refinement and Symbolic Computation of Average Case Bound. | Hong Yi Chen, Supratik Mukhopadhyay, Zheng Lu |
| 2013 | Looking at Mean-Payoff and Total-Payoff through Windows. | Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, Jean-Franois Raskin |
| 2013 | Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points. | Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Jol Ouaknine, Jean-Franois Raskin, James Worrell |
| 2013 | SmacC: A Retargetable Symbolic Execution Engine. | Armin Biere, Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2013 | A Framework for Ranking Vacuity Results. | Shoham Ben-David, Orna Kupferman |