| 2009 | A Tableau Calculus for Regular Grammar Logics with Converse. | Linh Anh Nguyen, Andrzej Szalas |
| 2009 | Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. | Sean McLaughlin, Frank Pfenning |
| 2009 | Volume Computation for Boolean Combination of Linear Arithmetic Constraints. | Feifei Ma, Sheng Liu, Jian Zhang |
| 2009 | Fair Derivations in Monodic Temporal Reasoning. | Michel Ludwig, Ullrich Hustadt |
| 2009 | Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2009 | Interpolation and Symbol Elimination. | Laura Kovcs, Andrei Voronkov |
| 2009 | Beyond Dependency Graphs. | Martin Korp, Aart Middeldorp |
| 2009 | Instantiation-Based Automated Reasoning: From Theory to Practice. | Konstantin Korovin |
| 2009 | System Description: H-PILoT. | Carsten Ihlemann, Viorica Sofronie-Stokkermans |
| 2009 | Decidability Results for Saturation-Based Model Building. | Matthias Horbach, Christoph Weidenbach |
| 2009 | Does This Set of Clauses Overlap with at Least One MUS? | ric Grgoire, Bertrand Mazure, Cdric Piette |
| 2009 | An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. | Rajeev Gor, Florian Widmann |
| 2009 | Ground Interpolation for Combined Theories. | Amit Goel, Sava Krstic, Cesare Tinelli |
| 2009 | A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. | Stephan Falke, Deepak Kapur |
| 2009 | Complexity of Fractran and Productivity. | Jrg Endrullis, Clemens Grabmayer, Dimitri Hendriks |
| 2009 | Automated Inference of Finite Unsatisfiability. | Koen Claessen, Ann Lilliestrm |
| 2009 | Computing Knowledge in Security Protocols under Convergent Equational Theories. | Stefan Ciobaca, Stphanie Delaune, Steve Kremer |
| 2009 | Interpolant Generation for UTVPI. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2009 | veriT: An Open, Trustable and Efficient SMT-Solver. | Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Dharbe, Pascal Fontaine |
| 2009 | Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. | Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodrguez-Carbonell, Albert Rubio |
| 2009 | On Deciding Satisfiability by DPLL(G+ | Maria Paola Bonacina, Christopher Lynch, Leonardo Mendona de Moura |
| 2009 | A Generalization of Semenov's Theorem to Automata over Real Numbers. | Bernard Boigelot, Julien Brusten, Jrme Leroux |
| 2009 | Dei: A Theorem Prover for Terms with Integer Exponents. | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2009 | Superposition and Model Evolution Combined. | Peter Baumgartner, Uwe Waldmann |
| 2008 | Contextual Rewriting in SPASS. | Christoph Weidenbach, Patrick Wischnewski |