| 2016 | CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions. | Marco Rocchetto, Nils Ole Tippenhauer |
| 2016 | Scaling BDD-based Timed Verification with Simulation Reduction. | Truong Khanh Nguyen, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen, Jin Song Dong |
| 2016 | Automated Requirements Validation for ATP Software via Specification Review and Testing. | Weikai Miao, Geguang Pu, Yinbo Yao, Ting Su, Danzhu Bao, Yang Liu, Shuohao Chen, Kunpeng Xiong |
| 2016 | Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic. | Francesco Marconi, Marcello M. Bersani, Madalina Erascu, Matteo Rossi |
| 2016 | Concolic Unbounded-Thread Reachability via Loop Summaries. | Peizun Liu, Thomas Wahl |
| 2016 | A Formal Approach to Identifying Security Vulnerabilities in Telecommunication Networks. | Linas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver, Silke Holtmanns |
| 2016 | Partial Order Reduction for State/Event Systems. | Shuanglong Kan, Zhiqiu Huang, Zhe Chen |
| 2016 | Session-Based Compositional Analysis for Actor-Based Languages Using Futures. | Eduard Kamburjan, Crystal Chang Din, Tzu-Chun Chen |
| 2016 | Proving Event-B Models with Reusable Generic Lemmas. | Alexei Iliasov, Paulius Stankaitis, Alexander B. Romanovsky |
| 2016 | Multi-threaded On-the-Fly Model Generation of Malware with Hash Compaction. | Minh Hai Nguyen, Quan Thanh Tho, Le Duc Anh |
| 2016 | Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder. | Saurabh Gadia, Cyrille Artho, Gedare Bloom |
| 2016 | Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. | Mohammed Foughali, Bernard Berthomieu, Silvano Dal-Zilio, Flix Ingrand, Anthony Mallet |
| 2016 | Local Livelock Analysis of Component-Based Models. | Madiel S. Conserva Filho, Marcel Vincius Medeiros Oliveira, Augusto Sampaio, Ana Cavalcanti |
| 2016 | Contextual Trace Refinement for Concurrent Objects: Safety and Progress. | Brijesh Dongol, Lindsay Groves |
| 2016 | Service Adaptation with Probabilistic Partial Models. | Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun, Jin Song Dong |
| 2016 | A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case. | Valentin Cassano, Thomas Stephen Edward Maibaum, Silviya Grigorova |
| 2016 | Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks. | Richard Banach, Michael J. Butler |
| 2016 | A System Substitution Mechanism for Hybrid Systems in Event-B. | Guillaume Babin, Yamine At Ameur, Neeraj Kumar Singh, Marc Pantel |
| 2016 | Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa's Case (Extended Abstract). | Keijiro Araki, Taro Kurita |
| 2016 | Decision Problems for Parametric Timed Automata. | tienne Andr, Didier Lime, Olivier H. Roux |
| 2016 | Checking SysML Models for Co-simulation. | Nuno Amlio, Richard John Payne, Ana Cavalcanti, Jim Woodcock |
| 2016 | Formal Availability Analysis Using Theorem Proving. | Waqar Ahmad, Osman Hasan |
| 2015 | Formalization and Verification of Declarative Cloud Orchestration. | Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi |
| 2015 | A Predictability Algorithm for Distributed Discrete Event Systems. | Lina Ye, Philippe Dague, Farid Nouioua |
| 2015 | An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. | Shuling Wang, Naijun Zhan, Liang Zou |