| 2005 | Flat Counter Automata Almost Everywhere! | Jrme Leroux, Grgoire Sutre |
| 2005 | State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method. | Charles A. Lakos, Lars Michael Kristensen |
| 2005 | Formal Construction and Verification of Home Service Robots: A Case Study. | Moonzoo Kim, Kyo Chul Kang |
| 2005 | Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems. | Geng-Dian Huang, Farn Wang |
| 2005 | An Approach for the Verification of SystemC Designs Using AsmL. | Ali Habibi, Sofine Tahar |
| 2005 | Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. | Guy Edward Gallasch, Jonathan Billington |
| 2005 | Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. | Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster |
| 2005 | Semi-automatic Distributed Synthesis. | Bernd Finkbeiner, Sven Schewe |
| 2005 | Syntactical Colored Petri Nets Reductions. | Sami Evangelista, Serge Haddad, Jean-Franois Pradat-Peyre |
| 2005 | Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach. | Abhishek Dubey, Xianbin Wu, Hang Su, Tak-John Koo |
| 2005 | Reasoning About Transfinite Sequences. | Stphane Demri, David Nowak |
| 2005 | Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. | Werner Damm, Guilherme Pinto, Stefan Ratschan |
| 2005 | Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. | Pierre Combes, David Harel, Hillel Kugler |
| 2005 | Decomposition-Based Verification of Cyclic Workflows. | Yongsun Choi, J. Leon Zhao |
| 2005 | Termination and Invariance Analysis of Loops. | Aaron R. Bradley, Zohar Manna |
| 2005 | Synthesis of Interface Automata. | Purandar Bhaduri |
| 2005 | Comparison of Different Semantics for Time Petri Nets. | Batrice Brard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux |
| 2005 | Flat Acceleration in Symbolic Model Checking. | Sbastien Bardin, Alain Finkel, Jrme Leroux, Philippe Schnoebelen |
| 2004 | Toward Unbounded Model Checking for Region Automata. | Fang Yu, Bow-Yaw Wang |
| 2004 | First-Order LTL Model Checking Using MDGs. | Fang Wang, Sofine Tahar, Otmane At Mohamed |
| 2004 | A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata. | Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teruo Higashino |
| 2004 | Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity. | Bai Su, Wenhui Zhang |
| 2004 | Synthesising Attacks on Cryptographic Protocols. | David Sinclair, David Gray, Geoff W. Hamilton |
| 2004 | Localizing Errors in Counterexample with Iteratively Witness Searching. | ShengYu Shen, Ying Qin, Sikun Li |
| 2004 | Modular Model Checking of Software Specifications with Simultaneous Environment Generation. | Claudio de la Riva, Javier Tuya |