| 2007 | The Complexity of Temporal Logic with Until and Since over Ordinals. | Stphane Demri, Alexander Rabinovich |
| 2007 | Protocol Verification Via Rigid/Flexible Resolution. | Stphanie Delaune, Hai Lin, Christopher Lynch |
| 2007 | Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap. | Francien Dechesne, Mohammad Reza Mousavi, Simona Orzan |
| 2007 | Mechanized Verification of CPS Transformations. | Zaynah Dargaye, Xavier Leroy |
| 2007 | Deciding Knowledge in Security Protocols for Monoidal Equational Theories. | Vronique Cortier, Stphanie Delaune |
| 2007 | Verifying Cryptographic Protocols with Subterms Constraints. | Yannick Chevalier, Denis Lugiez, Michal Rusinowitch |
| 2007 | Matching in Hybrid Terminologies. | Sebastian Brandt |
| 2007 | Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. | Richard Bonichon, David Delahaye, Damien Doligez |
| 2007 | HORPO with Computability Closure: A Reconstruction. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2007 | Completeness and Decidability in Sequence Logic. | Marc Bezem, Tore Langholm, Michal Walicki |
| 2007 | The Semantics of Consistency and Trust in Peer Data Exchange Systems. | Leopoldo E. Bertossi, Loreto Bravo |
| 2007 | Least and Greatest Fixed Points in Linear Logic. | David Baelde, Dale Miller |
| 2007 | Monadic Fragments of Gdel Logics: Decidability and Undecidability Results. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller |
| 2007 | Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic. | Roland Axelsson, Martin Lange |
| 2007 | Extending a Resolution Prover for Inequalities on Elementary Functions. | Behzad Akbarpour, Lawrence C. Paulson |
| 2007 | One-Pass Tableaux for Computation Tree Logic. | Pietro Abate, Rajeev Gor, Florian Widmann |
| 2007 | Decidable Fragments of Many-Sorted Logic. | Aharon Abadi, Alexander Moshe Rabinovich, Mooly Sagiv |
| 2006 | A Local System for Intuitionistic Logic. | Alwen Tiu |
| 2006 | An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. | Carsten Schrmann, Mark-Oliver Stehr |
| 2006 | Sequential, Parallel, and Quantified Updates of First-Order Structures. | Philipp Rmmer |
| 2006 | Context-Sensitive Multivariant Assertion Checking in Modular Programs. | Pawel Pietrzak, Jess Correas, Germn Puebla, Manuel V. Hermenegildo |
| 2006 | A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes. | Boris Motik, Ulrike Sattler |
| 2006 | Derivational Complexity of Knuth-Bendix Orders Revisited. | Georg Moser |
| 2006 | Verification Condition Generation Via Theorem Proving. | John Matthews, J Strother Moore, Sandip Ray, Daron Vroon |
| 2006 | Deciding Satisfiability of Positive Second Order Joinability Formulae. | Sbastien Limet, Pierre Pillot |