| 2016 | A Cognitive Framework Based on Rewriting Logic for the Analysis of Interactive Systems. Antonio Cerone |
| 2016 | Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems - (Extended Abstract). Gul Agha |
| 2016 | Automatic Derivation of Platform Noninterference Properties. Oliver Schwarz, Mads Dam |
| 2016 | BMotionWeb: A Tool for Rapid Creation of Formal Prototypes. Lukas Ladenberger, Michael Leuschel |
| 2016 | CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli |
| 2016 | Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams. Christian Dernehl, Norman Hansen, Stefan Kowalewski |
| 2016 | Combining Predicate Abstraction with Fixpoint Approximations. Tuba Yavuz |
| 2016 | Compliance Checking in the Open Payments Ecosystem. Shaun Azzopardi, Christian Colombo, Gordon J. Pace, Brian Vella |
| 2016 | Coq Implementation of OO Verification Framework VeriJ. Ke Zhang, Zongyan Qiu |
| 2016 | Correlating Structured Inputs and Outputs in Functional Specifications. Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer |
| 2016 | Counterexamples from Proof Failures in SPARK. David Hauzar, Claude Marché, Yannick Moy |
| 2016 | Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. Jaroslav Bendík, Nikola Benes, Jiri Barnat, Ivana Cerná |
| 2016 | Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information. Josselin Feist, Laurent Mounier, Marie-Laure Potet |
| 2016 | Incentive Stackelberg Mean-Payoff Games. Anshul Gupta, Sven Schewe, Ashutosh Trivedi, Sai Krishna Deepak Maram, Bharath Kumar Padarthi |
| 2016 | LTL Model Checking under Fairness in ProB. Ivaylo Dobrikov, Michael Leuschel, Daniel Plagge |
| 2016 | LTL Parameter Synthesis of Parametric Timed Automata. Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná |
| 2016 | Linearizability and Causality. Simon Doherty, John Derrick |
| 2016 | Model Checking Simulation Rules for Linearizability. Graeme Smith |
| 2016 | Modularizing Crosscutting Concerns in Component-Based Systems. Antoine El-Hokayem, Yliès Falcone, Mohamad Jaber |
| 2016 | Program Generation Using Simulated Annealing and Model Checking. Idress Husien, Sven Schewe |
| 2016 | Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution. Jera Hensel, Jürgen Giesl, Florian Frohn, Thomas Ströder |
| 2016 | Refinement-Based Verification of Communicating Unstructured Code. Nils Jähnig, Thomas Göthel, Sabine Glesner |
| 2016 | SMT-Based Automatic Proof of ASM Model Refinement. Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene |
| 2016 | Satisfiability Checking: Theory and Applications. Erika Ábrahám, Gereon Kremer |
| 2016 | Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings Rocco De Nicola, Eva Kühn |
| 2016 | Stability-Based Adaptation of Asynchronously Communicating Software. Carlos Canal, Gwen Salaün |
| 2016 | Tightening a Contract Refinement. Alessandro Cimatti, Ramiro Demasi, Stefano Tonetta |
| 2016 | Towards a Proof Framework for Information Systems with Weak Consistency. Peter Zeller, Arnd Poetzsch-Heffter |