| 2003 | Symmetry Reductions in Model-Checking. | A. Prasad Sistla |
| 2003 | Abstract Interpretation-Based Certification of Assembly Code. | Xavier Rival |
| 2003 | Software Model Checking with Abstraction Refinement. | Andreas Podelski |
| 2003 | Model-Checking and Abstraction to the Aid of Parameterized Systems. | Amir Pnueli, Lenore D. Zuck |
| 2003 | Formal Verification of the Horn-Preneel Micropayment Protocol. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2003 | Lifting Temporal Proofs through Abstractions. | Kedar S. Namjoshi |
| 2003 | Abstraction of Expectation Functions Using Gaussian Distributions. | David Monniaux |
| 2003 | Reasoning about Layered Message Passing Systems. | B. Meenakshi, Ramaswamy Ramanujam |
| 2003 | Property Checking Driven Abstract Interpretation-Based Static Analysis. | Damien Mass |
| 2003 | Action Refinement from a Logical Point of View. | Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher |
| 2003 | Types for Evolving Communication in Safe Ambients. | Francesca Levi |
| 2003 | Efficient Computation of Recurrence Diameters. | Daniel Kroening, Ofer Strichman |
| 2003 | Properties of a Type Abstract Interpreter. | Roberta Gori, Giorgio Levi |
| 2003 | On the Expressiveness of 3-Valued Models. | Patrice Godefroid, Radha Jagadeesan |
| 2003 | Domain Compression for Complete Abstractions. | Roberto Giacobazzi, Isabella Mastroeni |
| 2003 | Shape Analysis through Predicate Abstraction and Model Checking. | Dennis Dams, Kedar S. Namjoshi |
| 2003 | Automatic Verification by Abstract Interpretation. | Patrick Cousot |
| 2003 | CHASE: A Static Checker for JML's Assignable Clause. | Nstor Catao, Marieke Huisman |
| 2003 | Complexity of Nesting Analysis in Mobile Ambients. | Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza |
| 2003 | Bisimulation and Unwinding for Verifying Possibilistic Security Properties. | Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi |
| 2002 | Automatic Verification of Probabilistic Free Choice. | Lenore D. Zuck, Amir Pnueli, Yonit Kesten |
| 2002 | Storage Size Reduction by In-place Mapping of Arrays. | Remko Tronon, Maurice Bruynooghe, Gerda Janssens, Francky Catthoor |
| 2002 | Weak Muller Acceptance Conditions for Tree Automata. | Salvatore La Torre, Aniello Murano, Margherita Napoli |
| 2002 | A Simulation Preorder for Abstraction of Reactive Systems. | Ferucio Laurentiu Tiplea, Aurora Tiplea |
| 2002 | An Abstract Schema for Equivalence-Checking Games. | Li Tan |