| 2016 | Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. | Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover |
| 2016 | Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. | Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock |
| 2016 | Array Folds Logic. | Przemyslaw Daca, Thomas A. Henzinger, Andrey Kupriyanov |
| 2016 | A Decision Procedure for Sets, Binary Relations and Partial Functions. | Maximiliano Cristi, Gianfranco Rossi |
| 2016 | Hitting Families of Schedules for Asynchronous Programs. | Dmitry Chistikov, Rupak Majumdar, Filip Niksic |
| 2016 | The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach. | Yu-Fang Chen, Lei Song, Zhilin Wu |
| 2016 | Structural Synthesis for GXW Specifications. | Chih-Hong Cheng, Yassine Hamza, Harald Ruess |
| 2016 | Termination Analysis of Probabilistic Programs Through Positivstellensatz's. | Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady |
| 2016 | Studying Sequences of Jumps in Hybrid Systems to Detect Zeno Phenomenon. | Alexandre Chapoutot, Julien Alexandre Dit Sandretto |
| 2016 | The Kind 2 Model Checker. | Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli |
| 2016 | Symbolic Optimal Reachability in Weighted Timed Automata. | Patricia Bouyer, Maximilien Colange, Nicolas Markey |
| 2016 | Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. | Sylvie Boldo |
| 2016 | Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems. | Roderick Bloem, Nicolas Braud-Santoni, Swen Jacobs |
| 2016 | Solving Parity Games via Priority Promotion. | Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero |
| 2016 | Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory. | Sidi Mohamed Beillahi, Umair Siddique, Sofine Tahar |
| 2016 | Synthesizing Probabilistic Invariants via Doob's Decomposition. | Gilles Barthe, Thomas Espitau, Luis Mara Ferrer Fioriti, Justin Hsu |
| 2016 | Markov Chains and Unambiguous Bchi Automata. | Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klppelholz, David Mller, James Worrell |
| 2016 | Compositional Synthesis of Reactive Controllers for Multi-agent Systems. | Rajeev Alur, Salar Moarref, Ufuk Topcu |
| 2016 | Proving Properties on PWA Systems Using Copositive and Semidefinite Programming. | Assal Adj |
| 2016 | Stateless Model Checking for POWER. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson |
| 2016 | Verification of Networks of Smart Energy Systems over the Cloud. | Alessandro Abate |
| 2016 | Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2016 | Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses. | Dirk Beyer, Matthias Dangl |
| 2015 | Automatic Verification of Stability and Safety for Delay Differential Equations. | Liang Zou, Martin Frnzle, Naijun Zhan, Peter Nazier Mosaad |
| 2015 | Poling: SMT Aided Linearizability Proofs. | He Zhu, Gustavo Petri, Suresh Jagannathan |