| 2016 | Dealing with Incompleteness in Automata-Based Model Checking. | Claudio Menghi, Paola Spoletini, Carlo Ghezzi |
| 2016 | Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations. | Bjrnar Luteberget, Christian Johansen, Claus Feyling, Martin Steffen |
| 2016 | Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers. | Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu, Jiaguang Sun |
| 2016 | Automated Verification of Timed Security Protocols with Clock Drift. | Li Li, Jun Sun, Jin Song Dong |
| 2016 | SpecCert: Specifying and Verifying Hardware-Based Security Enforcement. | Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Nron, Benjamin Morin |
| 2016 | Explaining Relaxed Memory Models with Program Transformations. | Ori Lahav, Viktor Vafeiadis |
| 2016 | Towards Concolic Testing for Hybrid Systems. | Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun, Jingyi Wang |
| 2016 | Refactoring Refinement Structure of Event-B Machines. | Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden |
| 2016 | A Generic Logic for Proving Linearizability. | Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson |
| 2016 | Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow. | Yusuke Kawamoto, Fabrizio Biondi, Axel Legay |
| 2016 | Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller. | Yu Jiang, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, Lui Sha |
| 2016 | An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. | Zhe Hou, David Sann, Alwen Tiu, Yang Liu, Koh Chuen Hoa |
| 2016 | Error Invariants for Concurrent Traces. | Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies |
| 2016 | An Algebra of Synchronous Atomic Steps. | Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis |
| 2016 | Formalising and Validating the Interface Description in the FMI Standard. | Miran Hasanagic, Peter W. V. Tran-Jrgensen, Kenneth Lausdahl, Peter Gorm Larsen |
| 2016 | Mechanised Verification Patterns for Dafny. | Gudmund Grov, Yuhui Lin, Vytautas Tumas |
| 2016 | Modal Kleene Algebra Applied to Program Correctness. | Victor B. F. Gomes, Georg Struth |
| 2016 | Learning Moore Machines from Input-Output Traces. | Georgios Giantamidis, Stavros Tripakis |
| 2016 | Exploring Model Quality for ACAS X. | Dimitra Giannakopoulou, Dennis Guck, Johann Schumann |
| 2016 | Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. | Antonio Flores-Montoya |
| 2016 | Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. | Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lnn |
| 2016 | Recovering High-Level Conditions from Binary Programs. | Adel Djoudi, Sbastien Bardin, ric Goubault |
| 2016 | Finding Suitable Variability Abstractions for Family-Based Analysis. | Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski |
| 2016 | Local Planning of Multiparty Interactions with Bounded Horizons. | Mahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem |
| 2016 | Danger Invariants. | Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis |