| 2002 | A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa |
| 2002 | A Fully Abstract Model for Higher-Order Mobile Ambients. Mario Coppo, Mariangiola Dezani-Ciancaglini |
| 2002 | A Refinement of the Escape Property. Patricia M. Hill, Fausto Spoto |
| 2002 | A Simulation Preorder for Abstraction of Reactive Systems. Ferucio Laurentiu Tiplea, Aurora Tiplea |
| 2002 | An Abstract Schema for Equivalence-Checking Games. Li Tan |
| 2002 | An Experiment in Type Inference and Verification by Abstract Interpretation. Roberta Gori, Giorgio Levi |
| 2002 | Analyzing Cryptographic Protocols in a Reactive Framework. R. K. Shyamasundar |
| 2002 | Approximating ATL Aidan Harding, Mark Ryan, Pierre-Yves Schobbens |
| 2002 | Automata-Theoretic Decision of Timed Games. Marco Faella, Salvatore La Torre, Aniello Murano |
| 2002 | Automatic Verification of Probabilistic Free Choice. Lenore D. Zuck, Amir Pnueli, Yonit Kesten |
| 2002 | Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode. Cinzia Bernardeschi, Nicoletta De Francesco |
| 2002 | Combining Norms to Prove Termination. Samir Genaim, Michael Codish, John P. Gallagher, Vitaly Lagoon |
| 2002 | Compositional Termination Analysis of Symbolic Forward Analysis. Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski |
| 2002 | Improving the Encoding of LTL Model Checking into SAT. Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani |
| 2002 | Model Checking Modal Transition Systems Using Kripke Structures. Michael Huth |
| 2002 | Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. Kai Baukus, Yassine Lakhnech, Karsten Stahl |
| 2002 | Proofs Methods for Bisimulation Based Information Flow Security. Riccardo Focardi, Carla Piazza, Sabina Rossi |
| 2002 | Static Monotonicity Analysis for lambda-definable Functions over Lattices. Andrzej S. Murawski, Kwangkeun Yi |
| 2002 | Storage Size Reduction by In-place Mapping of Arrays. Remko Tronçon, Maurice Bruynooghe, Gerda Janssens, Francky Catthoor |
| 2002 | Synchronous Closing of Timed SDL Systems for Model Checking. Natalia Sidorova, Martin Steffen |
| 2002 | Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers Agostino Cortesi |
| 2002 | Verifying BDD Algorithms through Monadic Interpretation. Sava Krstic, John Matthews |
| 2002 | Weak Muller Acceptance Conditions for Tree Automata. Salvatore La Torre, Aniello Murano, Margherita Napoli |