| 2003 | Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. | Sanjit A. Seshia, Randal E. Bryant |
| 2003 | TRIM: A Tool for Triggered Message Sequence Charts. | Bikram Sengupta, Rance Cleaveland |
| 2003 | Certifying Optimality of State Estimation Programs. | Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean |
| 2003 | Calculating-Confluence Compositionally. | Gordon J. Pace, Frdric Lang, Radu Mateescu |
| 2003 | Fast Mu-Calculus Model Checking when Tree-Width Is Bounded. | Jan Obdrzlek |
| 2003 | Abstraction for Branching Time Properties. | Kedar S. Namjoshi |
| 2003 | Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). | Leonardo Mendona de Moura, Harald Rue, Maria Sorea |
| 2003 | Interpolation and SAT-Based Model Checking. | Kenneth L. McMillan |
| 2003 | A Symbolic Approach to Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
| 2003 | Deductive Verification of Advanced Out-of-Order Microprocessors. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion. | Yonit Kesten, Nir Piterman, Amir Pnueli |
| 2003 | Domain-Specific Optimization in Automata Learning. | Hardi Hungar, Oliver Niese, Bernhard Steffen |
| 2003 | Thread-Modular Abstraction Refinement. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer |
| 2003 | Abstraction and BDDs Complement SAT-Based BMC in DiVer. | Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar |
| 2003 | A Work-Efficient Distributed Algorithm for Reachability Analysis. | Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2003 | Model Checking Conformance with Scenario-Based Specifications. | Marcelo Glusman, Shmuel Katz |
| 2003 | An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. | Marc Geilen |
| 2003 | Theorem Proving Using Lazy Proof Explication. | Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe |
| 2003 | Reasoning with Temporal Logic on Truncated Paths. | Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout |
| 2003 | Monitoring Temporal Rules Combined with Time Series. | Doron Drusinsky |
| 2003 | Evidence Explorer: A Tool for Exploring Model-Checking Proofs. | Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka |
| 2003 | Linear Invariant Generation Using Non-linear Constraint Solving. | Michael Coln, Sriram Sankaranarayanan, Henny Sipma |
| 2003 | Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2003 | Structural Symbolic CTL Model Checking of Asynchronous Systems. | Gianfranco Ciardo, Radu Siminiceanu |
| 2003 | TLQSolver: A Temporal Logic Query Checker. | Marsha Chechik, Arie Gurfinkel |