| 2017 | First order temporal logic monitoring with BDDs. | Klaus Havelund, Doron Peled, Dogan Ulus |
| 2017 | Automated repair by example for firewalls. | William T. Hallahan, Ennan Zhai, Ruzica Piskac |
| 2017 | K-induction without unrolling. | Arie Gurfinkel, Alexander Ivrii |
| 2017 | Efficient generation of all minimal inductive validity cores. | Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek |
| 2017 | Safety verification of phaser programs. | Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng |
| 2017 | Sampling invariants from frequency distributions. | Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodk |
| 2017 | FuseIC3: An algorithm for checking large design spaces. | Rohit Dureja, Kristin Yvonne Rozier |
| 2017 | Tagged BDDs: Combining reduction rules from different decision diagram types. | Tom van Dijk, Robert Wille, Robert Meolic |
| 2017 | Automatic verification of application-tailored OSEK kernels. | Hans-Peter Deifel, Merlin Gttlinger, Stefan Milius, Lutz Schrder, Christian Dietrich, Daniel Lohmann |
| 2017 | Symbolic security analysis using the Tamarin prover. | Cas Cremers |
| 2017 | Automated formal reasoning about AWS systems. | Byron Cook |
| 2017 | FAR-Cubicle - A new reachability algorithm for Cubicle. | Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux |
| 2017 | SMT-based analysis of switching multi-domain linear Kirchhoff networks. | Alessandro Cimatti, Sergio Mover, Mirko Sessa |
| 2017 | Learning to prove safety over parameterised concurrent systems. | Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rmmer |
| 2017 | Hardware model checking competition 2017. | Armin Biere, Tom van Dijk, Keijo Heljanko |
| 2017 | Z3str3: A string solver with theory-aware heuristics. | Murphy Berzish, Vijay Ganesh, Yunhui Zheng |
| 2017 | Learning support sets in IC3 and Quip: The good, the bad, and the ugly. | Ryan Berryhill, Alexander Ivrii, Neil Veira, Andreas G. Veneris |
| 2017 | Exact quantitative probabilistic model checking through rational search. | Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan |
| 2017 | Verification of a lazy cache coherence protocol against a weak memory model. | Christopher J. Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul B. Jackson, Vijay Nagarajan |
| 2017 | Modular SMT-based analysis of nonlinear hybrid systems. | Kyungmin Bae, Sicun Gao |
| 2017 | Duality-based interpolation for quantifier-free equalities and uninterpreted functions. | Leonardo Alt, Antti Eero Johannes Hyvrinen, Sepideh Asadi, Natasha Sharygina |
| 2017 | Coalition, intrigue, ambush, destruction and pride: Herding cats can be challenging. | Jade Alglave |
| 2016 | Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems. | Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donz, Sanjit A. Seshia |
| 2016 | Network verification - When Clarke meets Cerf. | George Varghese |
| 2016 | Lazy sequentialization for TSO and PSO via shared memory abstractions. | Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |