| 2003 | A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution. Ping Yang, C. R. Ramakrishnan, Scott A. Smolka |
| 2003 | Abstract Interpretation-Based Certification of Assembly Code. Xavier Rival |
| 2003 | Abstraction of Expectation Functions Using Gaussian Distributions. David Monniaux |
| 2003 | Action Refinement from a Logical Point of View. Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher |
| 2003 | Automatic Verification by Abstract Interpretation. Patrick Cousot |
| 2003 | Behavior-Based Model Construction. Bernhard Steffen, Hardi Hungar |
| 2003 | Bisimulation and Unwinding for Verifying Possibilistic Security Properties. Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi |
| 2003 | CHASE: A Static Checker for JML's Assignable Clause. Néstor Cataño, Marieke Huisman |
| 2003 | Complexity of Nesting Analysis in Mobile Ambients. Chiara Braghin, Agostino Cortesi, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza |
| 2003 | Domain Compression for Complete Abstractions. Roberto Giacobazzi, Isabella Mastroeni |
| 2003 | Efficient Computation of Recurrence Diameters. Daniel Kroening, Ofer Strichman |
| 2003 | Efficient Verification of Timed Automata with BDD-Like Data-Structures. Farn Wang |
| 2003 | Formal Verification of the Horn-Preneel Micropayment Protocol. Kazuhiro Ogata, Kokichi Futatsugi |
| 2003 | Lifting Temporal Proofs through Abstractions. Kedar S. Namjoshi |
| 2003 | Model-Checking and Abstraction to the Aid of Parameterized Systems. Amir Pnueli, Lenore D. Zuck |
| 2003 | On the Expressiveness of 3-Valued Models. Patrice Godefroid, Radha Jagadeesan |
| 2003 | Optimized Live Heap Bound Analysis. Leena Unnikrishnan, Scott D. Stoller, Yanhong A. Liu |
| 2003 | Properties of a Type Abstract Interpreter. Roberta Gori, Giorgio Levi |
| 2003 | Property Checking Driven Abstract Interpretation-Based Static Analysis. Damien Massé |
| 2003 | Reasoning about Layered Message Passing Systems. B. Meenakshi, Ramaswamy Ramanujam |
| 2003 | Shape Analysis through Predicate Abstraction and Model Checking. Dennis Dams, Kedar S. Namjoshi |
| 2003 | Software Model Checking with Abstraction Refinement. Andreas Podelski |
| 2003 | Symmetry Reductions in Model-Checking. A. Prasad Sistla |
| 2003 | Types for Evolving Communication in Safe Ambients. Francesca Levi |
| 2003 | Using Simulated Execution in Verifying Distributed Algorithms. Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch |
| 2003 | Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay |