| 2013 | Lazy Abstractions for Timed Automata. | Frdric Herbreteau, B. Srivathsan, Igor Walukiewicz |
| 2013 | Software Model Checking for People Who Love Automata. | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2013 | Validating Library Usage Interactively. | William R. Harris, Guoliang Jin, Shan Lu, Somesh Jha |
| 2013 | On the Termination of Positive Supercompilation. | Geoff W. Hamilton |
| 2013 | SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. | Christoph Haase, Samin Ishtiaq, Jol Ouaknine, Matthew J. Parkinson |
| 2013 | Proving Termination Starting from the End. | Pierre Ganty, Samir Genaim |
| 2013 | Transforming Undecidable Synthesis Problems into Decidable Problems. | Bernd Finkbeiner |
| 2013 | Duet: Static Analysis for Unbounded Parallelism. | Azadeh Farzan, Zachary Kincaid |
| 2013 | Program Repair without Regret. | Christian von Essen, Barbara Jobstmann |
| 2013 | A Fully Verified Executable LTL Model Checker. | Javier Esparza, Peter Lammich, Ren Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | Parameterized Verification of Asynchronous Shared-Memory Systems. | Javier Esparza, Pierre Ganty, Rupak Majumdar |
| 2013 | Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. | Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger |
| 2013 | Efficient Robust Monitoring for STL. | Alexandre Donz, Thomas Ferrre, Oded Maler |
| 2013 | Explain: A Tool for Performing Abductive Inference. | Isil Dillig, Thomas Dillig |
| 2013 | Equivalence of Extended Symbolic Finite Transducers. | Loris D'Antoni, Margus Veanes |
| 2013 | Generating Non-linear Interpolants by Semidefinite Programming. | Liyun Dai, Bican Xia, Naijun Zhan |
| 2013 | Towards Distributed Software Model-Checking Using Decision Diagrams. | Maximilien Colange, Souheib Baarir, Fabrice Kordon, Yann Thierry-Mieg |
| 2013 | Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. | Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Qinsi Wang |
| 2013 | A Tool for Estimating Information Leakage. | Tom Chothia, Yusuke Kawamoto, Chris Novakovic |
| 2013 | Lengths May Break Privacy - Or How to Check for Equivalences with Length. | Vincent Cheval, Vronique Cortier, Antoine Plet |
| 2013 | JBernstein: A Validity Checker for Generalized Polynomial Constraints. | Chih-Hong Cheng, Harald Ruess, Natarajan Shankar |
| 2013 | Flow*: An Analyzer for Non-linear Hybrid Systems. | Xin Chen, Erika brahm, Sriram Sankaranarayanan |
| 2013 | Faster Algorithms for Markov Decision Processes with Low Treewidth. | Krishnendu Chatterjee, Jakub Lacki |
| 2013 | Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. | Krishnendu Chatterjee, Andreas Gaiser, Jan Kretnsk |
| 2013 | A Scalable and Nearly Uniform Generator of SAT Witnesses. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |