Program

Wednesday, September 14

9:00-10:00 Invited Talk 1 - Program Analysis and Machine Learning: A Win-Win Deal
Sriram Rajamani, Microsoft Research India

10:00-10:30 Coffee Break

10:30-12:30 Session 1 - Heap Analysis (Chair: Thomas Reps)

Purity Analysis: An Abstract Interpretation Formulation
Ravichandran Madhavan, Ganesan Ramalingam and Kapil Vaswani. [slides]
The Complexity of Abduction for Separated Heap Abstractions
Nikos Gorogiannis, Max Kanovich and Peter O'Hearn. [slides]
Efficient Decision Procedures for Heaps using STRAND
P. Madhusudan and Xiaokang Qiu. [slides]
The Flow-Insensitive Precision of Andersen's Analysis in Practice
Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan and Manu Sridharan. [slides]

12:30-14:00 Lunch Break

14:00-15:00 Invited Talk 2 - Combining Algebraic Domains and Logical Theories by the Reduced Product
Patrick Cousot, Ecole normale superieure, Paris & Courant Institute of Mathematical sciences, New York University [slides]

15:00-15:30 Coffee Break

15:30 - 17:00 Session 2 - Static Analysis with Applications (Chair: Matthieu Martel)

Side-Effect Analysis of Assembly Code
Andrea Flexeder, Michael Petter and Helmut Seidl. [slides]
Directed symbolic execution
Kin-Keung Ma, Yit Phang Khoo, Jeffrey S. Foster and Michael Hicks. [slides]
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri and Cindy Rubio Gonzalez. [slides]

Thursday, September 15

9:00-10:00 Invited Talk 3 - Program Analysis for Web Security
John Mitchell, Stanford

10:00-10:30 Coffee Break

10:30-12:30 Session 3 - Concurrency (Chair: Noam Rinetzky)

On Sequentializing Concurrent Programs
Ahmed Bouajjani, Michael Emmi and Gennaro Parlato. [slides]
Verifying Fence Elimination Optimisations
Viktor Vafeiadis and Francesco Zappa Nardelli. [slides]
An Efficient Static Trace Simplification Technique for Debugging Concurrent Programs
Jeff Huang and Charles Zhang [slides]
A family of abstract interpretations for static analysis of concurrent higher-order programs Matthew Might and David Van Horn. [slides]

12:30-14:00 Lunch Break

14:00-15:00 Invited Talk 4 - Astrée: Design and Experience
Daniel Kaestner, AbsInt, Germany

15:30-17:00 Session 4 - Numerical Domains (Chair: Antoine Mine)

Abstract Domains of Affine Relations
Matt Elder, Junghee Lim, Tushar Sharma, Tycho Andersen and Thomas Reps. [slides]
Transitive Closures of Affine Integer Tuple Relations and their Overapproximations
Sven Verdoolaege, Albert Cohen and Anna Beletska. [slides]
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs
Peter Schrammel and Bertrand Jeannet. [slides]

17:00-17:20 Break

17:20-18:00 Concert

20:30-     Conference Dinner

Friday, September 16

9:00-10:00 Invited Talk 5 - Formal Model Reduction
Jerome Feret, Ecole Normale Superieure, France [slides]

10:00-10:30 Coffee Break

10:30-12:30 Session 5 - Medley (Chair: Roberto Giacobazzi)

Invisible Invariants and Abstract Interpretation
Kenneth Mcmillan and Lenore Zuck. [slides]
An Abstraction-Refinement Framework for Trigger Querying
Guy Avni and Orna Kupferman. [slides]
Bound Analysis of Imperative Programs with the Size-change Abstraction
Florian Zuleger, Moritz Sinn, Sumit Gulwani and Helmut Veith. [slides]
Satisfiability Modulo Recursive Programs
Philippe Suter, Ali Sinan Köksal and Viktor Kuncak. [slides]

12:00-14:00 Extended Lunch Break (starts at 12:00)

14:00-15:00 Session 6 - Probabilistic Analysis (Chair: Ganesan Ramalingam)

Probabilistic Analysis of Perforated Patterns
Sasa Misailovic, Daniel Roy and Martin Rinard.
Probabilistic Abstractions with Arbitrary Domains
Javier Esparza and Andreas Gaiser. [slides]

15:00-15:30 Coffee Break

15:30-16:30 Session 7 - Bounded Model Checking (Chair: Noam Rinetzky)

Software Verification Using k-Induction
Alastair Donaldson, Leopold Haller, Daniel Kroening and Philipp Ruemmer.
Using bounded model checking to focus fixpoint iterations
David Monniaux and Laure Gonnord. [slides]

Invited Talk - Interpolation and Widening
Ken McMillan, Microsoft Research [slides]