| 2008 | A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking. | Nick Moffat, Michael Goldsmith, Bill Roscoe |
| 2008 | Decomposition for Compositional Verification. | Bjrn Metzler, Heike Wehrheim, Daniel Wonisch |
| 2008 | A Practical Approach to Partiality - A Proof Based Approach. | Farhad Mehta |
| 2008 | Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool. | Michael Leuschel, Marc Fontaine |
| 2008 | How Can We Make Industry Adopt Formal Methods? | Takuya Katayama |
| 2008 | Program Models for Compositional Verification. | Marieke Huisman, Irem Aktug, Dilian Gurov |
| 2008 | Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. | John Hatcliff |
| 2008 | Practical Automated Partial Verification of Multi-paradigm Real-Time Models. | Carlo A. Furia, Matteo Pradella, Matteo Rossi |
| 2008 | A Unified Model Checking Approach with Projection Temporal Logic. | Zhenhua Duan, Cong Tian |
| 2008 | An Approach to Testing with Embedded Context Using Model Checker. | Lihua Duan, Jessica Chen |
| 2008 | Specifying and Verifying Sensor Networks: An Experiment of Formal Methods. | Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang |
| 2008 | Modelling and Proof of a Tree-Structured File System in Event-B and Rodin. | Kriangsak Damchoom, Michael J. Butler, Jean-Raymond Abrial |
| 2008 | A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm. | Florin Craciun, Shengchao Qin, Wei-Ngan Chin |
| 2008 | Correct Channel Passing by Construction. | Chao Cai, Zongyan Qiu, Xiangpeng Zhao, Hongli Yang |
| 2008 | Towards Abstraction for DynAlloy Specifications. | Nazareno Aguirre, Marcelo F. Frias, Pablo Ponzio, Brian J. Cardiff, Juan P. Galeotti, Germn Regis |
| 2007 | Model Checking with SAT-Based Characterization of ACTL Formulas. | Wenhui Zhang |
| 2007 | Formalizing SANE Virtual Processor in Thread Algebra. | Thuy Duong Vu, Chris R. Jesshope |
| 2007 | Model Checking Propositional Projection Temporal Logic Based on SPIN. | Cong Tian, Zhenhua Duan |
| 2007 | Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking. | Guillermo Rodrguez-Navas, Julin Proenza, Hans Hansson |
| 2007 | A Denotational Semantics for Handel-C Hardware Compilation. | Juan Ignacio Perna, Jim Woodcock |
| 2007 | Automatic Generation of Verified Concurrent Hardware. | Marcel Oliveira, Jim Woodcock |
| 2007 | Calculating and Composing Progress Properties in Terms of the Leads-to Relation. | Arjan J. Mooij |
| 2007 | Challenges in Software Certification. | T. S. E. Maibaum |
| 2007 | Integrating Specification-Based Review and Testing for Detecting Errors in Programs. | Shaoying Liu |
| 2007 | VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System. | Jacques Julliand, Hassan Mountassir, Emilie Oudot |