| 2006 | Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. | Sylvie Boldo |
| 2006 | Cut-Simulation in Impredicative Logics. | Christoph Benzmller, Chad E. Brown, Michael Kohlhase |
| 2006 | Dynamic Logic with Non-rigid Functions. | Bernhard Beckert, Andr Platzer |
| 2006 | Blocking and Other Enhancements for Bottom-Up Model Generation Methods. | Peter Baumgartner, Renate A. Schmidt |
| 2006 | CEL - A Polynomial-Time Reasoner for Life Science Ontologies. | Franz Baader, Carsten Lutz, Boontawee Suntisrivaraporn |
| 2005 | The Decidability of the First-Order Theory of Knuth-Bendix Order. | Ting Zhang, Henny B. Sipma, Zohar Manna |
| 2005 | Computer Search for Counterexamples to Wilkie's Identity. | Jian Zhang |
| 2005 | A Combination Method for Generating Interpolants. | Greta Yorsh, Madanlal Musuvathi |
| 2005 | On the Complexity of Equational Horn Clauses. | Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick |
| 2005 | Nominal Techniques in Isabelle/HOL. | Christian Urban, Christine Tasson |
| 2005 | Regular Protocols and Attacks with Regular Knowledge. | Tomasz Truderung |
| 2005 | Deduction with XOR Constraints in Security API Modelling. | Graham Steel |
| 2005 | Hierarchic Reasoning in Local Theory Extensions. | Viorica Sofronie-Stokkermans |
| 2005 | KRHyper - In Your Pocket. | Alex Sinner, Thomas Kleemann |
| 2005 | Tabling for Higher-Order Logic Programming. | Brigitte Pientka |
| 2005 | Proving Properties of Incremental Merkle Trees. | Mizuhito Ogawa, Eiichi Horita, Satoshi Ono |
| 2005 | System Description: Multi A Multi-strategy Proof Planner. | Andreas Meier, Erica Melis |
| 2005 | A Proof-Producing Decision Procedure for Real Arithmetic. | Sean McLaughlin, John Harrison |
| 2005 | Well-Nested Context Unification. | Jordi Levy, Joachim Niehren, Mateu Villaret |
| 2005 | Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. | Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh |
| 2005 | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. | Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard |
| 2005 | Temporal Logics over Transitive States. | Boris Konev, Frank Wolter, Michael Zakharyaschev |
| 2005 | Deciding Monodic Fragments by Temporal Resolution. | Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
| 2005 | Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. | Guillem Godoy, Ashish Tiwari |
| 2005 | Model Representation via Contexts and Implicit Generalizations. | Christian G. Fermller, Reinhard Pichler |