| 2016 | Robots at the Edge of the Cloud. | Rupak Majumdar |
| 2016 | Partial Order Reduction for Event-Driven Multi-threaded Programs. | Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar |
| 2016 | JDart: A Dynamic Symbolic Analysis Framework. | Kasper Se Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, Vishwanath Raman |
| 2016 | CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution). | Stefan Lwe |
| 2016 | Abstract Learning Frameworks for Synthesis. | Christof Lding, P. Madhusudan, Daniel Neider |
| 2016 | Developing and Debugging Proof Strategies by Tinkering. | Yuhui Lin, Pierre Le Bras, Gudmund Grov |
| 2016 | Online and Compositional Learning of Controllers with Application to Floor Heating. | Kim G. Larsen, Marius Mikucionis, Marco Muiz, Jir Srba, Jakob Haahr Taankvist |
| 2016 | Characteristic Formulae for Session Types. | Julien Lange, Nobuko Yoshida |
| 2016 | PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games. | Marta Kwiatkowska, David Parker, Clemens Wiltsche |
| 2016 | Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution). | Michal Kotoun, Petr Peringer, Veronika Sokov, Toms Vojnar |
| 2016 | PTIME Computation of Transitive Closures of Octagonal Relations. | Filip Konecn |
| 2016 | LPI: Software Verification with Local Policy Iteration - (Competition Contribution). | Egor George Karpenkov |
| 2016 | Safety-Constrained Reinforcement Learning for MDPs. | Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen |
| 2016 | PrDK: Protocol Programming with Automata. | Sung-Shik T. Q. Jongmans, Farhad Arbab |
| 2016 | Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. | Radu Iosif, Adam Rogalewicz, Toms Vojnar |
| 2016 | Run Forester, Run Backwards! - (Competition Contribution). | Luks Holk, Martin Hruska, Ondrej Lengl, Adam Rogalewicz, Jir Simcek, Toms Vojnar |
| 2016 | Ultimate Automizer with Two-track Proofs - (Competition Contribution). | Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schtzle, Andreas Podelski |
| 2016 | Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution). | Henning Gnther, Alfons Laarman, Georg Weissenbacher |
| 2016 | Tactics for the Dafny Program Verifier. | Gudmund Grov, Vytautas Tumas |
| 2016 | An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation. | Jan Friso Groote, Anton Wijs |
| 2016 | Interpolants in Nonlinear Theories Over the Reals. | Sicun Gao, Damien Zufferey |
| 2016 | CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution). | Karlheinz Friedberger |
| 2016 | Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). | Cdric Favre, Hagen Vlzer, Peter Mller |
| 2016 | Coqoon - An IDE for Interactive Proof Development in Coq. | Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink |
| 2016 | DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation. | Hugues Evrard |