| 2017 | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi |
| 2017 | Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT. Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang |
| 2017 | Bringing LTL Model Checking to Biologists. Zara Ahmed, David Benqué, Sergey Berezin, Anna Caroline E. Dahl, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Jay Nanavati, Nir Piterman, Maik Riechert, Nikita Skoblov |
| 2017 | Complete Abstractions and Subclassical Modal Logics. Vijay Victor D'Silva, Marcelo Sousa |
| 2017 | Conjunctive Abstract Interpretation Using Paramodulation. Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv |
| 2017 | Counterexample Validation and Interpolation-Based Refinement for Forest Automata. Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Tomás Vojnar |
| 2017 | Detecting All High-Level Dataraces in an RTOS Kernel. Suvam Mukherjee, Arun Kumar, Deepak D'Souza |
| 2017 | Detecting Strict Aliasing Violations in the Wild. Pascal Cuoq, Loïc Runarvot, Alexander Cherepanov |
| 2017 | Dynamic Reductions for Model Checking Concurrent Software. Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher |
| 2017 | Effective Bug Finding in C Programs with Shape and Effect Abstractions. Iago Abal, Claus Brabrand, Andrzej Wasowski |
| 2017 | Efficient Elimination of Redundancies in Polyhedra by Raytracing. Alexandre Maréchal, Michaël Périn |
| 2017 | Finding Relevant Templates via the Principal Component Analysis. Yassamine Seladji |
| 2017 | IC3 - Flipping the E in ICE. Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik |
| 2017 | Independence Abstractions and Models of Concurrency. Vijay Victor D'Silva, Daniel Kroening, Marcelo Sousa |
| 2017 | Matching Multiplications in Bit-Vector Formulas. Supratik Chakraborty, Ashutosh Gupta, Rahul Jain |
| 2017 | Partitioned Memory Models for Program Analysis. Wei Wang, Clark W. Barrett, Thomas Wies |
| 2017 | Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions. Raphaël Monat, Antoine Miné |
| 2017 | Property Directed Reachability for Proving Absence of Concurrent Modification Errors. Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham |
| 2017 | Reachability for Dynamic Parametric Processes. Anca Muscholl, Helmut Seidl, Igor Walukiewicz |
| 2017 | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. Andrew Reynolds, Radu Iosif, Cristina Serban |
| 2017 | Reduction of Workflow Nets for Generalised Soundness Verification. Hadrien Bride, Olga Kouchnarenko, Fabien Peureux |
| 2017 | Solving Nonlinear Integer Arithmetic with MCSAT. Dejan Jovanovic |
| 2017 | Sound Bit-Precise Numerical Domains. Tushar Sharma, Thomas W. Reps |
| 2017 | Stabilizing Floating-Point Programs Using Provenance Analysis. Yijia Gu, Thomas Wahl |
| 2017 | Static Analysis of Communicating Processes Using Symbolic Transducers. Vincent Botbol, Emmanuel Chailloux, Tristan Le Gall |
| 2017 | Structuring Abstract Interpreters Through State and Value Abstractions. Sandrine Blazy, David Bühler, Boris Yakobowski |
| 2017 | Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang |
| 2017 | Synthesizing Non-Vacuous Systems. Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman |
| 2017 | Using Abstract Interpretation to Correct Synchronization Faults. Pietro Ferrara, Omer Tripp, Peng Liu, Eric Koskinen |
| 2017 | Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings Ahmed Bouajjani, David Monniaux |