| 2017 | A Context-Sensitive Memory Model for Verification of C/C++ Programs. Arie Gurfinkel, Jorge A. Navas |
| 2017 | A Gradual Interpretation of Union Types. Matías Toro, Éric Tanter |
| 2017 | A New Abstraction Framework for Affine Transformers. Tushar Sharma, Thomas W. Reps |
| 2017 | Abstract Semantic Diffing of Evolving Concurrent Programs. Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2017 | Combining Forward and Backward Abstract Interpretation of Horn Clauses. Alexey Bakhirkin, David Monniaux |
| 2017 | Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic. Lukás Holík, Roland Meyer, Tomás Vojnar, Sebastian Wolff |
| 2017 | Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification. Isabella Mastroeni, Michele Pasqua |
| 2017 | Incremental Analysis for Probabilistic Programs. Jieyuan Zhang, Yulei Sui, Jingling Xue |
| 2017 | Learning Shape Analysis. Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow |
| 2017 | Loop Invariants from Counterexamples. Marius Greitschus, Daniel Dietsch, Andreas Podelski |
| 2017 | Modular Demand-Driven Analysis of Semantic Difference for Program Versions. Anna Trostanetski, Orna Grumberg, Daniel Kroening |
| 2017 | Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2017 | Probabilistic Horn Clause Verification. Aws Albarghouthi |
| 2017 | Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains. Abdelraouf Ouadjaout, Antoine Miné |
| 2017 | Relative Store Fragments for Singleton Abstraction. Leandro Facchinetti, Zachary Palmer, Scott F. Smith |
| 2017 | Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. Alexandre Maréchal, David Monniaux, Michaël Périn |
| 2017 | Securing the SSA Transform. Chaoqiang Deng, Kedar S. Namjoshi |
| 2017 | Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings Francesco Ranzato |
| 2017 | Synthesizing Imperative Programs from Examples Guided by Static Analysis. Sunbeom So, Hakjoo Oh |
| 2017 | Template Polyhedra with a Twist. Sriram Sankaranarayanan, Mohamed Amin Ben Sassi |
| 2017 | Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky |
| 2017 | Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration. Colas Le Guernic |
| 2017 | Verifying Array Manipulating Programs by Tiling. Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat |