| 2012 | State Space c-Reductions of Concurrent Systems in Rewriting Logic. | Alberto Lluch-Lafuente, Jos Meseguer, Andrea Vandin |
| 2012 | Automatic Generation of Provably Correct Embedded Systems. | Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong |
| 2012 | A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification. | Mengjun Li |
| 2012 | Variable Permissions for Concurrency Verification. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2012 | SMT-Based False Positive Elimination in Static Program Analysis. | Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp |
| 2012 | Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS. | Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa |
| 2012 | The Confinement Problem in the Presence of Faults. | William L. Harrison, Adam M. Procter, Gerard Allwein |
| 2012 | Time Constraints with Temporal Logic Programming. | Meng Han, Zhenhua Duan, Xiaobing Wang |
| 2012 | Towards a Formal Verification Methodology for Collective Robotic Systems. | Edmond Gjondrekaj, Michele Loreti, Rosario Pugliese, Francesco Tiezzi, Carlo Pinciroli, Manuele Brambilla, Mauro Birattari, Marco Dorigo |
| 2012 | Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers. | Svetoslav R. Ganov, Sarfraz Khurshid, Dewayne E. Perry |
| 2012 | Formal Methods in the Aerospace Industry: Follow the Money. | Darren D. Cofer |
| 2012 | Verification of ATL Transformations Using Transformation Models and Model Finders. | Fabian Bttner, Marina Egea, Jordi Cabot, Martin Gogolla |
| 2012 | Equational Abstraction Refinement for Certified Tree Regular Model Checking. | Yohan Boichut, Benot Boyer, Thomas Genet, Axel Legay |
| 2012 | Separation Predicates: A Taste of Separation Logic in First-Order Logic. | Franois Bobot, Jean-Christophe Fillitre |
| 2012 | Towards Certified Runtime Verification. | Jan Olaf Blech, Ylis Falcone, Klaus Becker |
| 2012 | A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs. | Granville Barnett, Shengchao Qin |
| 2011 | Towards a Model Checker for NesC and Wireless Sensor Networks. | Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu |
| 2011 | Towards a Signal Calculus for Event-Based Synchronous Languages. | Yongxin Zhao, Jifeng He |
| 2011 | Domain-Driven Probabilistic Analysis of Programmable Logic Controllers. | Hehua Zhang, Yu Jiang, William N. N. Hung, Xiaoyu Song, Ming Gu |
| 2011 | The Safety-Critical Java Mission Model: A Formal Account. | Frank Zeyda, Ana Cavalcanti, Andy J. Wellings |
| 2011 | Integrating Prototyping into the SOFL Three-Step Modeling Approach. | Fauziah binti Zainuddin, Shaoying Liu |
| 2011 | Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures. | Fangfang Yuan, Stephen Wright, Kerstin Eder, David May |
| 2011 | Differencing Labeled Transition Systems. | Zhenchang Xing, Jun Sun, Yang Liu, Jin Song Dong |
| 2011 | Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. | Miroslav N. Velev, Ping Gao |
| 2011 | Verification of Orchestration Systems Using Compositional Partial Order Reduction. | Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong |