24th Static Analysis Symposium
August 30th - September 1st, 2017, New York City, NY, USA


The symposium and workshops will be held at the

    Courant Institute of Mathematical Studies (CIMS)

    New York University (NYU)

    Warren Weaver Hall (WWH or CIWW)

    251 Mercer Street

    New York, N.Y. 10012, USA


August 29th, 2017

August 30th - September 1st, 2017
August 29th - September 1st, 2017
August 31st, 2017

WWH 1302, 13th floor

WWH 317, 3rd floor

WWH 102, ground level (1st floor)

WWH 109, ground level (1st floor)

WWH 13th Floor Faculty Lounge

Torch Club, 18 Waverly Place

Tuesday, August 29th

09:00 - 17:00

Workshop Day

Wednesday, August 30th

09:00 - 10:00

Invited Talk 1

Reasoning with Permissions in Viper
Peter Müller

10:00 - 10:30

Session 1

Securing the SSA Transform
Chaoqiang Deng and Kedar Namjoshi

10:30 - 11:00

Coffee Break

11:00 - 12:30

Session 2 - Concurrency

Abstract (Semantic) Diffing of Evolving Concurrent Programs

Ahmed Bouajjani, Constantin Enea and Shuvendu Lahiri

Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza and Noam Rinetzky

Effect Summaries for Thread-Modular Analysis

Sebastian Wolff, Roland Meyer, Lukas Holik and Tomas Vojnar

12:30 - 14:00


14:00 - 15:00

Invited Tutorial 1

Static Program Analysis by Separation Logic
Josh Berdine

15:00 - 15:30

Session 3

Synthesizing Imperative Programs from Examples Guided by Static Analysis
Sunbeom So and Hakjoo Oh

15:30 - 16:00

Coffee Break

16:00 - 17:30

Session 4 - Memory Models and Shape Analysis

Portability Analysis for Weak Memory Models. Porthos: One Tool for all Models

Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko and Roland Meyer

A Context-Sensitive Memory Model for Verification of C/C++ Programs

Arie Gurfinkel and Jorge A. Navas

Learning Shape Analysis

Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna and Daniel Tarlow

Thursday, August 31st

09:00 - 10:00

Invited Talk 2

Proving Program Equality: Recent Progress and New Applications
Alex Aiken

10:00 - 10:30

Session 5

Verifying Array Manipulating Programs by Tiling
Divyesh Unadkat, Supratik Chakraborty and Ashutosh Gupta

10:30 - 11:00

Coffee Break

11:00 - 12:30

Session 6 - Probabilistic Models

Quantitative Static Analysis of Communication Protocols using Abstract Markov Chains

Abdelraouf Ouadjaout and Antoine Miné

Probabilistic Horn Clause Verification

Aws Albarghouthi

Incremental Analysis for Probabilistic programs

Jieyuan Zhang, Yulei Sui and Jingling Xue

12:30 - 14:00


14:00 - 15:00

Invited Tutorial 2

Abstract Interpretation for Program Security
Roberto Giacobazzi

15:00 - 15:30

Session 7

Modular Demand-Driven Analysis of Semantic Difference for Program Versions
Anna Trostanetski, Orna Grumberg and Daniel Kroening

15:30 - 16:00

Coffee Break

16:00 - 17:30

Session 8 - Loops and Types

Loop Invariants from Counterexamples

Marius Greitschus, Daniel Dietsch and Andreas Podelski

Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration

Colas Le Guernic

A Gradual Interpretation of Union Types

Matías Toro and Éric Tanter

Friday, September 1st

09:00 - 10:30

Session 9 - Numerical Domains

Template Polyhedra with a Twist

Sriram Sankaranarayanan and Mohamed Amin Ben Sassi

A new Abstraction Framework for Affine Transformers

Tushar Sharma and Thomas Reps

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming

Alexandre Maréchal, David Monniaux and Michael Perin

10:30 - 11:00

Coffee Break

11:00 - 12:30

Session 10 - Abstract Interpretation

Relative Store Fragments for Singleton Abstraction

Leandro Facchinetti, Zachary Palmer and Scott Smith

Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification

Isabella Mastroeni and Michele Pasqua
Combining Forward and Backward Abstract Interpretation of Horn Clauses

Alexey Bakhirkin and David Monniaux

12:30 - 14:00


14:00 - 15:00

Invited Talk 3

From Bug Bounty to Static Analysis
Francesco Logozzo