| 2017 | Minimization of Symbolic Transducers. | Olli Saarikivi, Margus Veanes |
| 2017 | STLInspector: STL Validation with Guarantees. | Hendrik Roehm, Thomas Heinz, Eva Charlotte Mayer |
| 2017 | Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. | Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli |
| 2017 | Introduction to the IEEE 1788-2015 Standard for Interval Arithmetic. | Nathalie Revol |
| 2017 | Markov Automata with Multiple Objectives. | Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen |
| 2017 | A Correct-by-Decision Solution for Simultaneous Place and Route. | Alexander Nadel |
| 2017 | Synchronization Synthesis for Network Programs. | Jedidiah McClurg, Hossein Hojjat, Pavol Cern |
| 2017 | Cutoff Bounds for Consensus Algorithms. | Ognjen Maric, Christoph Sprenger, David A. Basin |
| 2017 | Verified Computations Using Taylor Models and Their Applications. | Kyoko Makino, Martin Berz |
| 2017 | A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. | Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin |
| 2017 | Bounded Synthesis for Streett, Rabin, and \text CTL^*. | Ayrat Khalimov, Roderick Bloem |
| 2017 | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. | Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer |
| 2017 | Safety Verification of Deep Neural Networks. | Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu |
| 2017 | Verifying Equivalence of Spark Programs. | Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv |
| 2017 | Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis. | Adri Gascn, Ashish Tiwari, Brent Carmer, Umang Mathur |
| 2017 | Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems. | Marie Fortin, Anca Muscholl, Igor Walukiewicz |
| 2017 | EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. | Bernd Finkbeiner, Christopher Hahn, Marvin Stenger |
| 2017 | Studying the Numerical Quality of an Industrial Computing Code: A Case Study on Code_aster. | Franois Fvotte, Bruno Lathuilire |
| 2017 | Efficient Parallel Strategy Improvement for Parity Games. | John Fearnley |
| 2017 | BoSy: An Experimentation Framework for Bounded Synthesis. | Peter Faymonville, Bernd Finkbeiner, Leander Tentrup |
| 2017 | DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems. | Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan |
| 2017 | Network-Wide Configuration Synthesis. | Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin T. Vechev |
| 2017 | SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
| 2017 | Synthesis with Abstract Examples. | Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav |
| 2017 | A Storm is Coming: A Modern Probabilistic Model Checker. | Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk |