| 2017 | The Power of Symbolic Automata and Transducers. | Loris D'Antoni, Margus Veanes |
| 2017 | Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. | Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin T. Vechev |
| 2017 | Lagrangian Reachabililty. | Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul L. Jones, Scott A. Smolka, Radu Grosu |
| 2017 | A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. | Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clment Fumex |
| 2017 | A Study of Model-Order Reduction Techniques for Verification. | Yi Chou, Xin Chen, Sriram Sankaranarayanan |
| 2017 | Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. | Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar |
| 2017 | Non-polynomial Worst-Case Analysis of Recursive Programs. | Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady |
| 2017 | Data-Driven Synthesis of Full Probabilistic Programs. | Sarah E. Chasins, Phitchaya Mangpo Phothilimthana |
| 2017 | Sound Numerical Computations in Abstract Acceleration. | Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening |
| 2017 | Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. | Luca Cardelli, Milan Ceska, Martin Frnzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby |
| 2017 | Automated Resource Analysis with Coq Proof Objects. | Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao |
| 2017 | MightyL: A Compositional Translation from MITL to Timed Automata. | Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege |
| 2017 | Proving Linearizability Using Forward Simulations. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil |
| 2017 | Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. | Arthur Blot, Jean-Michel Muller, Laurent Thry |
| 2017 | Learning a Static Analyzer from Data. | Pavol Bielik, Veselin Raychev, Martin T. Vechev |
| 2017 | Rigorous Reachability Analysis and Domain Decomposition of Taylor Models. | Martin Berz, Kyoko Makino |
| 2017 | Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems. | Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safrnek |
| 2017 | On Multiphase-Linear Ranking Functions. | Amir M. Ben-Amram, Samir Genaim |
| 2017 | Towards Verifying Nonlinear Integer Arithmetic. | Paul Beame, Vincent Liew |
| 2017 | Runtime Verification of Temporal Properties over Out-of-Order Data Streams. | David A. Basin, Felix Klaedtke, Eugen Zalinescu |
| 2017 | Simulation-Equivalent Reachability of Large Linear Systems with Inputs. | Stanley Bak, Parasara Sridhar Duggirala |
| 2017 | Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees. | Stanley Bak, Sergiy Bogomolov, Thomas A. Henzinger, Aviral Kumar |
| 2017 | Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. | Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich |
| 2017 | Value Iteration for Long-Run Average Reward in Markov Decision Processes. | Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretnsk, Tobias Meggendorfer |
| 2017 | Verified Compilation of Space-Efficient Reversible Circuits. | Matthew Amy, Martin Roetteler, Krysta M. Svore |