| 2013 | Automatic Testing of Real-Time Graphics Systems. | Robert Nagy, Gerardo Schneider, Aram Timofeitchik |
| 2013 | Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution). | Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer |
| 2013 | Weighted Pushdown Systems with Indexed Weight Domains. | Yasuhiko Minamide |
| 2013 | PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. | Radu Mateescu, Gwen Salan |
| 2013 | CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution). | Stefan Lwe |
| 2013 | A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems. | Alexander Linden, Pierre Wolper |
| 2013 | Synthesis of Circular Compositional Program Proofs via Abduction. | Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv |
| 2013 | Model Checking Agent Knowledge in Dynamic Access Control Policies. | Masoud Koleini, Eike Ritter, Mark Ryan |
| 2013 | As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. | Jean-Francois Kempf, Marius Bozga, Oded Maler |
| 2013 | Integer Parameter Synthesis for Timed Automata. | Aleksandra Jovanovic, Didier Lime, Olivier H. Roux |
| 2013 | Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors. | Ajith K. John, Supratik Chakraborty |
| 2013 | Model-Checking Iterated Games. | Chung-Hao Huang, Sven Schewe, Farn Wang |
| 2013 | Ultimate Automizer with SMTInterpol - (Competition Contribution). | Matthias Heizmann, Jrgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski |
| 2013 | Runtime Verification Based on Register Automata. | Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos |
| 2013 | Analysis of Boolean Programs. | Patrice Godefroid, Mihalis Yannakakis |
| 2013 | Model Checking Database Applications. | Milos Gligoric, Rupak Majumdar |
| 2013 | Underapproximation of Procedure Summaries for Integer Programs. | Pierre Ganty, Radu Iosif, Filip Konecn |
| 2013 | Unbounded Model-Checking with Interpolation for Regular Language Constraints. | Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Sndergaard, Peter Schachte |
| 2013 | Policy Analysis for Self-administrated Role-Based Access Control. | Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato |
| 2013 | eVolCheck: Incremental Upgrade Checker for C. | Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina |
| 2013 | LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution). | Stephan Falke, Florian Merz, Carsten Sinz |
| 2013 | The Quest for Minimal Quotients for Probabilistic Automata. | Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang |
| 2013 | Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution). | Kamil Dudka, Petr Mller, Petr Peringer, Toms Vojnar |
| 2013 | An Overview of the mCRL2 Toolset and Its Recent Advances. | Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, Tim A. C. Willemse |
| 2013 | Ramsey vs. Lexicographic Termination Proving. | Byron Cook, Abigail See, Florian Zuleger |