| 2013 | Algebraic Laws for Process Subtyping. | Jos Dihego, Pedro R. G. Antonino, Augusto Sampaio |
| 2013 | The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software. | Giulia Costantini, Pietro Ferrara, Giuseppe Maggiore, Agostino Cortesi |
| 2013 | Verification of Functional and Non-functional Requirements of Web Service Composition. | Manman Chen, Tian Huat Tan, Jun Sun, Yang Liu, Jun Pang, Xiaohong Li |
| 2013 | A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification. | Gustavo Carvalho, Augusto Sampaio, Alexandre Mota |
| 2013 | Formally Verified System Initialisation. | Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell |
| 2013 | Reconstructing Paths for Reachable Code. | Stephan Arlt, Zhiming Liu, Martin Schf |
| 2013 | A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems. | tienne Andr, Benot Barbot, Clement Demoulins, Lom-Messan Hillah, Francis Hulin-Hubard, Fabrice Kordon, Alban Linard, Laure Petrucci |
| 2012 | A Concurrent Temporal Programming Model with Atomic Blocks. | Xiaoxiao Yang, Yu Zhang, Ming Fu, Xinyu Feng |
| 2012 | Predicate Analysis with Block-Abstraction Memoization. | Daniel Wonisch, Heike Wehrheim |
| 2012 | Demonic Testing of Concurrent Programs. | Scott West, Sebastian Nanz, Bertrand Meyer |
| 2012 | More Anti-chain Based Refinement Checking. | Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li |
| 2012 | Modeling and Verification of Probabilistic Actor Systems Using pRebeca. | Mahsa Varshosaz, Ramtin Khosravi |
| 2012 | A Temporal Logic with Mean-Payoff Constraints. | Takashi Tomita, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki |
| 2012 | Toward Practical Application of Formal Methods in Software Lifecycle Processes. | Mario Tokoro |
| 2012 | Heuristic-Guided Abstraction Refinement for Concurrent Systems. | Nils Timm, Heike Wehrheim, Mike Czech |
| 2012 | Complementary Methodologies for Developing Hybrid Systems with Event-B. | Wen Su, Jean-Raymond Abrial, Huibiao Zhu |
| 2012 | Applying Term Rewriting to Speech Recognition of Numbers. | Robert E. Shostak |
| 2012 | An Analytical and Experimental Comparison of CSP Extensions and Tools. | Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho |
| 2012 | ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications. | Tanmoy Sarkar, Samik Basu, Johnny S. Wong |
| 2012 | Modular Verification of OO Programs with Interfaces. | Zongyan Qiu, Ali Hong, Yijing Liu |
| 2012 | Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic. | Kazuhiro Ogata, Thi Thanh Huyen Phan |
| 2012 | Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization. | Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong |
| 2012 | Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System. | Yoshinori Neya, Noriaki Yoshiura |
| 2012 | Quantitative Program Dependence Graphs. | Chunyan Mu |
| 2012 | Quantitative Analysis of Information Flow Using Theorem Proving. | Tarek Mhamdi, Osman Hasan, Sofine Tahar |