| 2006 | Higher-Order Termination: From Kruskal to Computability. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2006 | Lemma Learning in the Model Evolution Calculus. | Peter Baumgartner, Alexander Fuchs, Cesare Tinelli |
| 2006 | CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. | Gilles Barthe, Benjamin Grgoire, Fernando Pastawski |
| 2006 | Splitting on Demand in SAT Modulo Theories. | Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2006 | On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. | Christel Baier, Nathalie Bertrand, Philippe Schnoebelen |
| 2006 | An Incremental Approach to Abstraction-Carrying Code. | Elvira Albert, Puri Arenas, Germn Puebla |
| 2005 | Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees. | Yao Wu, Enrico Pontelli, Desh Ranjan |
| 2005 | Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. | Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta |
| 2005 | Reasoning About Incompletely Defined Programs. | Christoph Walther, Stephan Schweitzer |
| 2005 | A Unified Memory Model for Pointers. | Harvey Tuch, Gerwin Klein |
| 2005 | Model Checking Abstract State Machines with Answer Set Programming. | Calvin Kai Fan Tang, Eugenia Ternovska |
| 2005 | Experimental Evaluation of Classical Automata Constructions. | Deian Tabakov, Moshe Y. Vardi |
| 2005 | On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity. | Wieslaw Szwast, Lidia Tendera |
| 2005 | Comparative Similarity, Tree Automata, and Diophantine Equations. | Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev |
| 2005 | Another Complete Local Search Method for SAT. | Haiou Shen, Hantao Zhang |
| 2005 | The Theorema Environment for Interactive Proof Development. | Florina Piroi, Temur Kutsia |
| 2005 | On the Specification of Sequent Systems. | Elaine Pimentel, Dale Miller |
| 2005 | A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem. | Alessandro Dal Pal, Agostino Dovier, Enrico Pontelli |
| 2005 | Monotone AC-Tree Automata. | Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, Yves Roos |
| 2005 | Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. | Robert Nieuwenhuis, Albert Oliveras |
| 2005 | Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. | Gopalan Nadathur, Xiaochu Qi |
| 2005 | An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures. | Angelo Montanari, Alberto Policriti, Nicola Vitacolonna |
| 2005 | Towards Automated Proof Support for Probabilistic Distributed Systems. | Annabelle McIver, Tjark Weber |
| 2005 | Satisfiability Checking for PC(ID). | Maarten Marin, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe |
| 2005 | Termination of Fair Computations in Term Rewriting. | Salvador Lucas, Jos Meseguer |