| 2012 | Reachability Modulo Theory Library. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | Escape to Mizar from ATPs. | Jesse Alama |
| 2011 | CSI - A Confluence Tool. | Harald Zankl, Bertram Felgenhauer, Aart Middeldorp |
| 2011 | AC Completion with Termination Tools. | Sarah Winkler, Aart Middeldorp |
| 2011 | An Efficient Decision Procedure for Imperative Tree Data Structures. | Thomas Wies, Marco Muiz, Viktor Kuncak |
| 2011 | Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving. | Michael Schneider, Geoff Sutcliffe |
| 2011 | Translating between Language and Logic: What Is Easy and What Is Difficult. | Aarne Ranta |
| 2011 | Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. | Andr Platzer |
| 2011 | Static Analysis of Android Programs. | tienne Payet, Fausto Spoto |
| 2011 | A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. | Lars Noschinski, Fabian Emmes, Jrgen Giesl |
| 2011 | Efficient General Unification for XOR with Homomorphism. | Zhiqiang Liu, Christopher Lynch |
| 2011 | On Transfinite Knuth-Bendix Orders. | Laura Kovcs, Georg Moser, Andrei Voronkov |
| 2011 | Solving Systems of Linear Inequalities by Bound Propagation. | Konstantin Korovin, Andrei Voronkov |
| 2011 | Scala to the Power of Z3: Integrating SMT and Programming. | Ali Sinan Kksal, Viktor Kuncak, Philippe Suter |
| 2011 | A Hybrid Method for Probabilistic Satisfiability. | Pavel Klinov, Bijan Parsia |
| 2011 | Cutting to the Chase Solving Linear Integer Arithmetic. | Dejan Jovanovic, Leonardo Mendona de Moura |
| 2011 | System Description: SPASS-FD. | Matthias Horbach |
| 2011 | Predicate Completion for non-Horn Clause Sets. | Matthias Horbach |
| 2011 | Sine Qua Non for Large Theory Reasoning. | Krystof Hoder, Andrei Voronkov |
| 2011 | Automated Reasoning in | Volker Haarslev, Roberto Sebastiani, Michele Vescovi |
| 2011 | A Connection-Based Characterization of Bi-intuitionistic Validity. | Didier Galmiche, Daniel Mry |
| 2011 | Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms. | Matthew Fredrikson, Mihai Christodorescu, Somesh Jha |
| 2011 | Compression of Propositional Resolution Proofs via Partial Regularization. | Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo |
| 2011 | Exploiting Symmetry in SMT Problems. | David Dharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo |
| 2011 | Advances in Proving Program Termination and Liveness. | Byron Cook |