24th Static Analysis Symposium
August 30th - September 1st, 2017, New York City, NY, USA
proceedingsProgramme
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)
New York, N.Y. 10012, USA
Rooms
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
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
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
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
Lunch
14:00 - 15:00
Invited Talk 3
From Bug Bounty to Static Analysis
Francesco Logozzo