| 2016 | A Generic Logic for Proving Linearizability. Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson |
| 2016 | A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems. Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin, Zhiming Liu |
| 2016 | A Model Checking Approach to Discrete Bifurcation Analysis. Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek |
| 2016 | An Algebra of Synchronous Atomic Steps. Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis |
| 2016 | An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa |
| 2016 | An Implementation of Deflate in Coq. Christoph-Simon Senjak, Martin Hofmann |
| 2016 | Approximate Bisimulation and Discretization of Hybrid CSP. Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan |
| 2016 | Automated Mutual Explicit Induction Proof in Separation Logic. Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin |
| 2016 | Automated Verification of Timed Security Protocols with Clock Drift. Li Li, Jun Sun, Jin Song Dong |
| 2016 | Battery-Aware Scheduling in Low Orbit: The GomX-3 Case. Morten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krcál, Gilles Nies, Marvin Stenger |
| 2016 | Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge luis Sacchini, Hendrik Tews, Thomas Tuerk |
| 2016 | Compositional Parameter Synthesis. Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess |
| 2016 | Counter-Example Guided Program Verification. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep |
| 2016 | Danger Invariants. Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis |
| 2016 | Dealing with Incompleteness in Automata-Based Model Checking. Claudio Menghi, Paola Spoletini, Carlo Ghezzi |
| 2016 | Decoupling Abstractions of Non-linear Ordinary Differential Equations. Andrew Sogokon, Khalil Ghorbal, Taylor T. Johnson |
| 2016 | Discounted Duration Calculus. Heinrich Ody, Martin Fränzle, Michael R. Hansen |
| 2016 | Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham |
| 2016 | Error Invariants for Concurrent Traces. Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies |
| 2016 | Explaining Relaxed Memory Models with Program Transformations. Ori Lahav, Viktor Vafeiadis |
| 2016 | Exploring Model Quality for ACAS X. Dimitra Giannakopoulou, Dennis Guck, Johann Schumann |
| 2016 | FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, Anna Philippou |
| 2016 | Finding Suitable Variability Abstractions for Family-Based Analysis. Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski |
| 2016 | Finite Model Finding Using the Logic of Equality with Uninterpreted Functions. Amirhossein Vakili, Nancy A. Day |
| 2016 | Formal Verification of Multi-Paxos for Distributed Consensus. Saksham Chand, Yanhong A. Liu, Scott D. Stoller |
| 2016 | Formalising and Validating the Interface Description in the FMI Standard. Miran Hasanagic, Peter W. V. Tran-Jørgensen, Kenneth Lausdahl, Peter Gorm Larsen |
| 2016 | From Electrical Switched Networks to Hybrid Automata. Alessandro Cimatti, Sergio Mover, Mirko Sessa |
| 2016 | GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking. Anton Wijs, Thomas Neele, Dragan Bosnacki |
| 2016 | Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow. Yusuke Kawamoto, Fabrizio Biondi, Axel Legay |
| 2016 | Industrial-Strength Model-Based Testing of Safety-Critical Systems. Jan Peleska, Wen-ling Huang |
| 2016 | Learning Moore Machines from Input-Output Traces. Georgios Giantamidis, Stavros Tripakis |
| 2016 | Local Planning of Multiparty Interactions with Bounded Horizons. Mahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem |
| 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 | Model-Based Design of an Energy-System Embedded Controller Using Taste. Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta |
| 2016 | RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions. Teodor Stoenescu, Alin Stefanescu, Sorina Predut, Florentin Ipate |
| 2016 | Recovering High-Level Conditions from Binary Programs. Adel Djoudi, Sébastien Bardin, Éric Goubault |
| 2016 | Refactoring Refinement Structure of Event-B Machines. Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden |
| 2016 | Regression Verification for Unbalanced Recursive Functions. Ofer Strichman, Maor Veitsman |
| 2016 | Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations. Bjørnar Luteberget, Christian Johansen, Claus Feyling, Martin Steffen |
| 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 | Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn |
| 2016 | Sound and Complete Mutation-Based Program Repair. Bat-Chen Rothenberg, Orna Grumberg |
| 2016 | SpecCert: Specifying and Verifying Hardware-Based Security Enforcement. Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin |
| 2016 | State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI. Stanislav Böhm, Ondrej Meca, Petr Jancar |
| 2016 | Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers. Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu, Jiaguang Sun |
| 2016 | Tighter Reachability Criteria for Deadlock-Freedom Analysis. Pedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe |
| 2016 | Towards Concolic Testing for Hybrid Systems. Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun, Jingyi Wang |
| 2016 | Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation. Yuqi Chen, Christopher M. Poskitt, Jun Sun |
| 2016 | Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. Antonio Flores-Montoya |
| 2016 | Validated Simulation-Based Verification of Delayed Differential Dynamics. Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan |