| 2004 | Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains. | YoungMin Kwon, Gul Agha |
| 2004 | Counterexample Guided Abstraction Refinement Via Program Execution. | Daniel Kroening, Alex Groce, Edmund M. Clarke |
| 2004 | A CLP Approach to Modelling Systems. | Joxan Jaffar |
| 2004 | Model-Based Testing with Spec#. | Jonathan Jacky |
| 2004 | Deriving Probabilistic Semantics Via the 'Weakest Completion'. | Jifeng He, Carroll Morgan, Annabelle McIver |
| 2004 | Guiding Spin Simulation. | Nicolae Goga, Judi Romijn |
| 2004 | Tutorial on the RAISE Language, Method and Tools. | Chris George |
| 2004 | An Equational Calculus for Alloy. | Marcelo F. Frias, Carlos Lpez Pombo, Nazareno Aguirre |
| 2004 | Multi-prover Verification of C Programs. | Jean-Christophe Fillitre, Claude March |
| 2004 | Timed Patterns: TCOZ to Timed Automata. | Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi |
| 2004 | CSP Representation of Game Semantics for Second-Order Idealized Algol. | Aleksandar S. Dimovski, Ranko Lazic |
| 2004 | Tutorial: Software Model Checking. | Edmund M. Clarke, Daniel Kroening |
| 2004 | Formal Models for Web Navigations with Session Control and Browser Cache. | Jessica Chen, Xiaoshan Zhao |
| 2004 | From Durational Specifications to TLA Designs of Timed Automata. | Yifeng Chen, Zhiming Liu |
| 2004 | A Formal Monitoring-Based Framework for Software Development and Analysis. | Feng Chen, Marcelo d'Amorim, Grigore Rosu |
| 2004 | A General Model for Reachability Testing of Concurrent Programs. | Richard H. Carver, Yu Lei |
| 2004 | Faster Analysis of Formal Specifications. | Fabrice Bouquet, Bruno Legeard, Mark Utting, Nicolas Vacelet |
| 2004 | A Knowledge Based Analysis of Cache Coherence. | Kai Baukus, Ron van der Meyden |
| 2004 | Interactive Verification of UML State Machines. | Michael Balser, Simon Bumler, Alexander Knapp, Wolfgang Reif, Andreas Thums |
| 2004 | Software Model Checking Using Linear Constraints. | Alessandro Armando, Claudio Castellini, Jacopo Mantovani |
| 2004 | Verifying a File System Implementation. | Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard |
| 2004 | Formal Proof from UML Models. | Nuno Amlio, Susan Stepney, Fiona Polack |
| 2004 | Managing Verification Activities Using SVM. | Bill Aldrich, Ansgar Fehnker, Peter H. Feiler, Zhi Han, Bruce H. Krogh, Eric Lim, Shiva Sivashankar |
| 2004 | Implementing Dynamic Aggregations of Abstract Machines in the B Method. | Nazareno Aguirre, Juan Bicarregui, Lucio Guzmn, T. S. E. Maibaum |
| 2003 | The Common Semantic Constructs of XML Family. | Hong Li Yang, Jun Gang Han, Ke Gang Hao |