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

Preliminary Programme


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

Lunch


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

Lunch


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

Combining Forward and Backward Abstract Interpretation of Horn Clauses

Alexey Bakhirkin and David Monniaux

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


12:30 - 14:00

Lunch


14:00 - 15:00

Invited Talk 3


From Bug Bounty to Static Analysis
Francesco Logozzo