| 2005 | Algebraic Intruder Deductions. | David A. Basin, Sebastian Mdersheim, Luca Vigan |
| 2005 | Zap: Automated Theorem Proving for Software Analysis. | Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi |
| 2005 | On Interpolation in Existence Logics. | Matthias Baaz, Rosalie Iemhoff |
| 2005 | The nomore++ Approach to Answer Set Solving. | Christian Anger, Martin Gebser, Thomas Linke, Andr Neumann, Torsten Schaub |
| 2005 | Regular Derivations in Basic Superposition-Based Calculi. | Vladimir Aleksic, Anatoli Degtyarev |
| 2005 | Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics. | Wolfgang Ahrendt, Andreas Roth, Ralf Sasse |
| 2004 | BCiC: A System for Code Authentication and Verification. | Nathan Whitehead, Martn Abadi |
| 2004 | How to Fix It: Using Fixpoints in Different Contexts. | Igor Walukiewicz |
| 2004 | Automated Termination Analysis for Incompletely Defined Programs. | Christoph Walther, Stephan Schweitzer |
| 2004 | Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. | Helmut Seidl, Kumar Neeraj Verma |
| 2004 | A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. | Norbert Schirmer |
| 2004 | A Trichotomy in the Complexity of Propositional Circumscription. | Gustav Nordh |
| 2004 | Abstract DPLL and Abstract DPLL Modulo Theories. | Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | Weighted Answer Sets and Applications in Intelligence Analysis. | Davy Van Nieuwenborgh, Stijn Heymans, Dirk Vermeir |
| 2004 | A Generic Framework for Interprocedural Analyses of Numerical Properties. | Markus Mller-Olm, Helmut Seidl |
| 2004 | Second-Order Matching via Explicit Substitutions. | Flvio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincn |
| 2004 | On a Semantic Subsumption Test. | Jerzy Marcinkowski, Jan Otop, Grzegorz Stelmaszek |
| 2004 | Implementing Efficient Resource Management for Linear Logic Programming. | Pablo Lpez, Jeff Polakow |
| 2004 | Suitable Graphs for Answer Set Programming. | Thomas Linke, Vladimir Sarsakov |
| 2004 | Abstract Model Generation for Preprocessing Clause Sets. | Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa |
| 2004 | A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
| 2004 | How the Location of * Influences Complexity in Kleene Algebra with Tests. | Christopher Hardin |
| 2004 | The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp |
| 2004 | Combining Lists with Non-stably Infinite Theories. | Pascal Fontaine, Silvio Ranise, Calogero G. Zarba |
| 2004 | Nonmonotonic Description Logic Programs: Implementation and Experiments. | Thomas Eiter, Giovambattista Ianni, Roman Schindlauer, Hans Tompits |