| 2003 | A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. Sharon Shoham, Orna Grumberg |
| 2003 | A Symbolic Approach to Predicate Abstraction. Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
| 2003 | A Work-Efficient Distributed Algorithm for Reachability Analysis. Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2003 | Abstraction and BDDs Complement SAT-Based BMC in DiVer. Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar |
| 2003 | Abstraction for Branching Time Properties. Kedar S. Namjoshi |
| 2003 | Algorithmic Improvements in Regular Model Checking. Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso |
| 2003 | An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. Marc Geilen |
| 2003 | Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea |
| 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion. Yonit Kesten, Nir Piterman, Amir Pnueli |
| 2003 | Calculating-Confluence Compositionally. Gordon J. Pace, Frédéric Lang, Radu Mateescu |
| 2003 | Certifying Optimality of State Estimation Programs. Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean |
| 2003 | Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings Warren A. Hunt Jr., Fabio Somenzi |
| 2003 | Deductive Verification of Advanced Out-of-Order Microprocessors. Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | Dense Counter Machines and Verification Problems. Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro |
| 2003 | Digitizing Interval Duration Logic. Gaurav Chakravorty, Paritosh K. Pandya |
| 2003 | Domain-Specific Optimization in Automata Learning. Hardi Hungar, Oliver Niese, Bernhard Steffen |
| 2003 | Efficient Image Computation in Infinite State Model Checking. Constantinos Bartzis, Tevfik Bultan |
| 2003 | Enhanced Vacuity Detection in Linear Temporal Logic. Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi |
| 2003 | Evidence Explorer: A Tool for Exploring Model-Checking Proofs. Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka |
| 2003 | FAST: Fast Acceleration of Symbolikc Transition Systems. Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci |
| 2003 | Fast Mu-Calculus Model Checking when Tree-Width Is Bounded. Jan Obdrzálek |
| 2003 | HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn |
| 2003 | Hybrid Acceleration Using Real Vector Automata (Extended Abstract). Bernard Boigelot, Frédéric Herbreteau, Sébastien Jodogne |
| 2003 | Interpolation and SAT-Based Model Checking. Kenneth L. McMillan |
| 2003 | Iterating Transducers in the Large (Extended Abstract). Bernard Boigelot, Axel Legay, Pierre Wolper |
| 2003 | Linear Invariant Generation Using Non-linear Constraint Solving. Michael Colón, Sriram Sankaranarayanan, Henny Sipma |
| 2003 | Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2003 | Model Checking Conformance with Scenario-Based Specifications. Marcelo Glusman, Shmuel Katz |
| 2003 | Model Checking Multi-Agent Programs with CASP. Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael J. Wooldridge |
| 2003 | Modular Strategies for Infinite Games on Recursive Graphs. Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | Monitoring Temporal Rules Combined with Time Series. Doron Drusinsky |
| 2003 | Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. Dirk Beyer, Claus Lewerentz, Andreas Noack |
| 2003 | Reasoning with Temporal Logic on Truncated Paths. Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout |
| 2003 | Strengthening Invariants by Symbolic Consistency Testing. Husam Abu-Haimed, Sergey Berezin, David L. Dill |
| 2003 | Structural Symbolic CTL Model Checking of Asynchronous Systems. Gianfranco Ciardo, Radu Siminiceanu |
| 2003 | TLQSolver: A Temporal Logic Query Checker. Marsha Chechik, Arie Gurfinkel |
| 2003 | TRIM: A Tool for Triggered Message Sequence Charts. Bikram Sengupta, Rance Cleaveland |
| 2003 | Theorem Proving Using Lazy Proof Explication. Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe |
| 2003 | Thread-Modular Abstraction Refinement. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer |
| 2003 | Timed Control with Partial Observability. Patricia Bouyer, Deepak D'Souza, P. Madhusudan, Antoine Petit |
| 2003 | To Store or Not to Store. Gerd Behrmann, Kim Guldstrand Larsen, Radek Pelánek |
| 2003 | Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. Sanjit A. Seshia, Randal E. Bryant |