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