| 2013 | PRocH: Proof Reconstruction for HOL Light. | Cezary Kaliszyk, Josef Urban |
| 2013 | Initial Experiments on Deriving a Complete HOL Simplification Set. | Cezary Kaliszyk, Thomas Sternagel |
| 2013 | The Tree Width of Separation Logic with Recursive Definitions. | Radu Iosif, Adam Rogalewicz, Jir Simcek |
| 2013 | The 481 Ways to Split a Clause and Deal with Propositional Variables. | Krystof Hoder, Andrei Voronkov |
| 2013 | Verifying Refutations with Extended Resolution. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | Towards Modularly Comparing Programs Using Automated Theorem Provers. | Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Reblo |
| 2013 | External Tools for the Formal Proof of the Kepler Conjecture. | Thomas C. Hales |
| 2013 | Reuse in Software Verification by Abstract Method Calls. | Reiner Hhnle, Ina Schaefer, Richard Bubel |
| 2013 | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. | Nada Habli, Amy P. Felty |
| 2013 | An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description. | Rajeev Gor, Jimmy Thomson |
| 2013 | dReal: An SMT Solver for Nonlinear Theories over the Reals. | Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | Solving Difference Constraints over Modular Arithmetic. | Graeme Gange, Harald Sndergaard, Peter J. Stuckey, Peter Schachte |
| 2013 | One Logic to Use Them All. | Jean-Christophe Fillitre |
| 2013 | Hierarchical Combination. | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen |
| 2013 | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2013 | Tractable Inference Systems: An Extension with a Deducibility Predicate. | Hubert Comon-Lundh, Vronique Cortier, Guillaume Scerri |
| 2013 | Automating Inductive Proofs Using Theory Exploration. | Koen Claessen, Moa Johansson, Dan Rosn, Nicholas Smallbone |
| 2013 | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). | Zakaria Chihani, Dale Miller, Fabien Renaud |
| 2013 | Foundational Proof Certificates in First-Order Logic. | Zakaria Chihani, Dale Miller, Fabien Renaud |
| 2013 | A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. | Guillaume Burel |
| 2013 | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. | Chad E. Brown, Christine Rizkallah |
| 2013 | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. | Jasmin Christian Blanchette, Andrei Paskevich |
| 2013 | Redirecting Proofs by Contradiction. | Jasmin Christian Blanchette |
| 2013 | LEO-II Version 1.5. | Christoph Benzmller, Nik Sultana |
| 2013 | System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description Logic. | Markus Bender, Bjrn Pelzer, Claudia Schon |