| 2008 | Valigator: A Verification Tool with Bound and Invariant Generation. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs |
| 2008 | A Logic of Singly Indexed Arrays. | Peter Habermehl, Radu Iosif, Toms Vojnar |
| 2008 | Role Conjunctions in Expressive Description Logics. | Birte Glimm, Yevgeny Kazakov |
| 2008 | Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation. | John P. Gallagher, Mads Rosendahl |
| 2008 | Nominal Renaming Sets. | Murdoch James Gabbay, Martin Hofmann |
| 2008 | Data-Oblivious Stream Productivity. | Jrg Endrullis, Clemens Grabmayer, Dimitri Hendriks |
| 2008 | Reasoning Using Knots. | Thomas Eiter, Magdalena Ortiz, Mantas Simkus |
| 2008 | Alternation Elimination by Complementation (Extended Abstract). | Christian Dax, Felix Klaedtke |
| 2008 | Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. | Edmund M. Clarke |
| 2008 | A TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2008 | Focusing Strategies in the Sequent Calculus of Synthetic Connectives. | Kaustuv Chaudhuri |
| 2008 | Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates. | Witold Charatonik, Michal Wrona |
| 2008 | An Algorithmic Interpretation of a Deep Inference System. | Kai Brnnler, Richard McKinley |
| 2008 | Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification. | Davide Bresolin, Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco |
| 2008 | Discounted Properties of Probabilistic Pushdown Automata. | Toms Brzdil, Vclav Brozek, Jan Holecek, Antonn Kucera |
| 2008 | The Max-Atom Problem and Its Relevance. | Marc Bezem, Robert Nieuwenhuis, Enric Rodrguez-Carbonell |
| 2008 | The Variable Hierarchy for the Lattice -Calculus. | Walid Belkhir, Luigi Santocanale |
| 2008 | (LIA) - Model Evolution with Linear Integer Arithmetic Constraints. | Peter Baumgartner, Alexander Fuchs, Cesare Tinelli |
| 2008 | Interactive Verification of Concurrent Systems using Symbolic Execution. | Michael Balser, Simon Bumler, Wolfgang Reif, Gerhard Schellhorn |
| 2008 | A Formal Language for Cryptographic Pseudocode. | Michael Backes, Matthias Berg, Dominique Unruh |
| 2008 | Cut Elimination for First Order Gdel Logic by Hyperclause Resolution. | Matthias Baaz, Agata Ciabattoni, Christian G. Fermller |
| 2008 | Efficient Generation of Unsatisfiability Proofs and Cores in SAT. | Roberto Asn, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2008 | Distributed Consistency-Based Diagnosis. | Vincent Armant, Philippe Dague, Laurent Simon |
| 2008 | From One Session to Many: Dynamic Tags for Security Protocols. | Myrto Arapinis, Stphanie Delaune, Steve Kremer |
| 2008 | Reveal: A Formal Verification Tool for Verilog Designs. | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah |