| 2010 | Proof Obligation Generation and Discharging for Recursive Definitions in VDM. | Augusto Ribeiro, Peter Gorm Larsen |
| 2010 | Compensable WorkFlow Nets. | Fazle Rabbi, Hao Wang, Wendy MacCaull |
| 2010 | Verifying Heap-Manipulating Programs with Unknown Procedure Calls. | Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin |
| 2010 | Loop Invariant Synthesis in a Combined Domain. | Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin |
| 2010 | Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. | Iman Poernomo, Jeffrey Terrell |
| 2010 | A Combination of Forward and Backward Reachability Analysis Methods. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2010 | Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems. | Jos Meseguer, Peter Csaba lveczky |
| 2010 | Abstract Program Slicing: From Theory towards an Implementation. | Isabella Mastroeni, Durica Nikolic |
| 2010 | A Formal Verification Study on the Rotterdam Storm Surge Barrier. | Ken Madlener, Sjaak Smetsers, Marko C. J. D. van Eekelen |
| 2010 | Assume-Guarantee Reasoning with Local Specifications. | Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu |
| 2010 | API Conformance Verification for Java Programs. | Xin Li, H. James Hoover, Piotr Rudnicki |
| 2010 | A Semantic Model for Service Composition with Coordination Time Delays. | Natallia Kokash, Behnaz Changizi, Farhad Arbab |
| 2010 | Model-Driven Protocol Design Based on Component Oriented Modeling. | Prabhu Shankar Kaliappan, Hartmut Knig, Sebastian Schmerl |
| 2010 | Dynamic Resource Reallocation between Deployment Components. | Einar Broch Johnsen, Olaf Owe, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa |
| 2010 | Making Pattern- and Model-Based Software Development More Rigorous. | Denis Hatebur, Maritta Heisel |
| 2010 | Automating Cut-off for Multi-parameterized Systems. | Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan |
| 2010 | Reasoning about Safety and Progress Using Contracts. | Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton |
| 2010 | Automating Coinduction with Case Analysis. | Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu |
| 2010 | Fostering Proof Scores in CafeOBJ. | Kokichi Futatsugi |
| 2010 | Comparison of Model Checking Tools for Information Systems. | Marc Frappier, Benot Fraikin, Romain Chossart, Raphal Chane-Yack-Fa, Mohammed Ouenzar |
| 2010 | A Methodology for Automatic Diagnosability Analysis. | Jonathan Ezekiel, Alessio Lomuscio |
| 2010 | Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. | Johannes Eriksson, Ralph-Johan Back |
| 2010 | Making the Right Cut in Model Checking Data-Intensive Timed Systems. | Rdiger Ehlers, Michael Gerke, Hans-Jrg Peter |
| 2010 | Exploiting Partial Success in Applying Automated Formal Methods. | Matthew B. Dwyer |
| 2010 | An Improved Decision Procedure for Propositional Projection Temporal Logic. | Zhenhua Duan, Cong Tian |