| 2017 | A Language-Theoretic View on Network Protocols. Pierre Ganty, Boris Köpf, Pedro Valero |
| 2017 | An Equivalence Checking Framework for Array-Intensive Programs. Kunal Banerjee, Chittaranjan A. Mandal, Dipankar Sarkar |
| 2017 | Attacking the V: On the Resiliency of Adaptive-Horizon MPC. Ashish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang, Radu Grosu |
| 2017 | Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings Deepak D'Souza, K. Narayan Kumar |
| 2017 | Compositional Safety Refutation Techniques. Kumar Madhukar, Peter Schrammel, Mandayam K. Srivas |
| 2017 | Concurrent Program Verification with Invariant-Guided Underapproximation. Sumanth Prabhu, Peter Schrammel, Mandayam K. Srivas, Michael Tautschnig, Anand Yeolekar |
| 2017 | Dealing with Priorities and Locks for Concurrent Programs. Marcio Diaz, Tayssir Touili |
| 2017 | Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes. Jan Kretínský, Tobias Meggendorfer |
| 2017 | Exploiting Partial Knowledge for Efficient Model Analysis. Nuno Macedo, Alcino Cunha, Eduardo Pessoa |
| 2017 | Finding Polynomial Loop Invariants for Probabilistic Programs. Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia |
| 2017 | Fixing the State Budget: Approximation of Regular Languages with Small DFAs. Graeme Gange, Pierre Ganty, Peter J. Stuckey |
| 2017 | ForFET: A Formal Feature Evaluation Tool for Hybrid Systems. Antonio Anastasio Bruto da Costa, Pallab Dasgupta |
| 2017 | Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. Rüdiger Ehlers |
| 2017 | Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units. Elvio Gilberto Amparore, Marco Beccuti, Susanna Donatelli |
| 2017 | HyLeak: Hybrid Analysis Tool for Information Leakage. Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, Louis-Marie Traonouez |
| 2017 | JTDec: A Tool for Tree Decompositions in Soot. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Andreas Pavlogiannis |
| 2017 | Knowledge Transfer and Information Leakage in Protocols. Abdullah Abdul Khadir, Madhavan Mukund, S. P. Suresh |
| 2017 | Lifting CDCL to Template-Based Abstract Domains for Program Verification. Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham |
| 2017 | Liquid Types for Array Invariant Synthesis. Manuel Montenegro, Susana Nieva, Ricardo Peña, Clara Segura |
| 2017 | Loop Quasi-Invariant Chunk Detection. Jean-Yves Moyen, Thomas Rubiano, Thomas Seiller |
| 2017 | Maximum Resilience of Artificial Neural Networks. Chih-Hong Cheng, Georg Nührenberg, Harald Ruess |
| 2017 | May-Happen-in-Parallel Analysis with Returned Futures. Elvira Albert, Samir Genaim, Pablo Gordillo |
| 2017 | Model Checking of C and C++ with DIVINE 4. Zuzana Baranová, Jiri Barnat, Katarína Kejstová, Tadeás Kucera, Henrich Lauko, Jan Mrázek, Petr Rockai, Vladimír Still |
| 2017 | Precise Null Pointer Analysis Through Global Value Numbering. Ankush Das, Akash Lal |
| 2017 | Proving Absence of Starvation by Means of Abstract Interpretation and Model Checking. Helmut Seidl, Ralf Vogler |
| 2017 | SamaTulyata: An Efficient Path Based Equivalence Checking Tool. Soumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar, Chittaranjan A. Mandal |
| 2017 | Synthesis of Optimal Resilient Control Strategies. Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonín Kucera, Vojtech Rehák |
| 2017 | Synthesizing Invariants by Solving Solvable Loops. Steven de Oliveira, Saddek Bensalem, Virgile Prevosto |
| 2017 | Tests and Refutation. Mohammad Torabi Dashti, David A. Basin |
| 2017 | The Density of Linear-Time Properties. Bernd Finkbeiner, Hazem Torfah |
| 2017 | The Reach-Avoid Problem for Constant-Rate Multi-mode Systems. Shankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi |