| 2016 | A SAT-Based Counterexample Guided Method for Unbounded Synthesis. | Alexander Legg, Nina Narodytska, Leonid Ryzhyk |
| 2016 | Fast, Flexible, and Minimal CTL Synthesis via SMT. | Tobias Klenze, Sam Bayless, Alan J. Hu |
| 2016 | JayHorn: A Framework for Verifying Java programs. | Temesghen Kahsai, Philipp Rmmer, Huascar Sanchez, Martin Schf |
| 2016 | Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. | Bishoksan Kafle, John P. Gallagher, Jos F. Morales |
| 2016 | Souffl: On Synthesis of Program Analyzers. | Herbert Jordan, Bernhard Scholz, Pavle Subotic |
| 2016 | ParCoSS: Efficient Parallelized Compiled Symbolic Simulation. | Vladimir Herdt, Hoang Minh Le, Daniel Groe, Rolf Drechsler |
| 2016 | Learning-Based Assume-Guarantee Regression Verification. | Fei He, Shu Mao, Bow-Yaw Wang |
| 2016 | Falsification of Dynamical Systems - An Industrial Perspective. | Thomas Heinz |
| 2016 | A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. | Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang |
| 2016 | RV-Match: Practical Semantics-Based Program Analysis. | Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu |
| 2016 | PSI: Exact Symbolic Inference for Probabilistic Programs. | Timon Gehr, Sasa Misailovic, Martin T. Vechev |
| 2016 | Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. | Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier |
| 2016 | XSat: A Fast Floating-Point Satisfiability Solver. | Zhoulai Fu, Zhendong Su |
| 2016 | BDD-Based Boolean Functional Synthesis. | Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi |
| 2016 | Combining Model Learning and Model Checking to Analyze TCP Implementations. | Paul Fiterau-Brostean, Ramon Janssen, Frits W. Vaandrager |
| 2016 | Bounded Cycle Synthesis. | Bernd Finkbeiner, Felix Klein |
| 2016 | Property Directed Equivalence via Abstract Simulation. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2016 | Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2. | Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Parasara Sridhar Duggirala |
| 2016 | Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2016 | Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits. | Hassan Eldib, Meng Wu, Chao Wang |
| 2016 | Slugs: Extensible GR(1) Synthesis. | Rdiger Ehlers, Vasumathi Raman |
| 2016 | Parsimonious, Simulation Based Verification of Linear Systems. | Parasara Sridhar Duggirala, Mahesh Viswanathan |
| 2016 | Effectively Propositional Interpolants. | Samuel Drews, Aws Albarghouthi |
| 2016 | Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances. | Michael Dooley, Fabio Somenzi |
| 2016 | Qlose: Program Repair with Quantitative Objectives. | Loris D'Antoni, Roopsha Samanta, Rishabh Singh |