23rd Static Analysis Symposium (SAS)

September 8--10, 2016, Edinburgh, UK

Preliminary Programme

Thursday, 8th of September, 2016, 8:45-9:00 : Welcome Session (James Cheney and Xavier Rival)

Thursday, 8th of September, 2016, 9:00-10:00 : Invited Talk (Session Chair: Manuel Hermenegildo)

• Martin Vechev :
  Learning from Programs: Probabilistic Models, Program Analysis and Synthesis

Thursday, 8th of September, 2016, 10:00-10:30 : Coffee Break

Thursday, 8th of September, 2016, 10:30-12:00 : Abstract Domains (Session Chair: Roberto Giacobazzi)

• Abstract Interpretation of Supermodular Games.
  Francesco Ranzato.
• A Parametric Abstract Domain for Lattice-Valued Regular Expressions.
  Jan Midtgaard, Flemming Nielson and Hanne Riis Nielson.
• Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Program.
  Matthieu Journault and Antoine Miné.

Thursday, 8th of September, 2016, 12:00-13:30 : Lunch

Thursday, 8th of September, 2016, 13:30-15:00 : Pointer Analysis (Session Chair: Francesco Ranzato)

• Structure-Sensitive Points-To Analysis for C and C++.
  George Balatsouras and Yannis Smaragdakis.
• Making k-Object-Sensitive Pointer Analysis More Precise with Still k-Limiting.
  Tian Tan, Yue Li and Jingling Xue.
• Flow and Context Sensitive Points-to Analysis using Generalized Points-to Graphs.
  Pritam Gharat, Uday Khedker and Alan Mycroft.

Thursday, 8th of September, 2016, 15:00-15:30 : Coffee Break

Thursday, 8th of September, 2016, 15:30-17:30 : Program Analysis (Session Chair: Caterina Urban)

• Learning a Variable-Clustering Strategy for Octagon From Labeled Data Generated by a Static Analysis.
  Kihong Heo, Hakjoo Oh and Hongseok Yang.
• On the linear ranking problem for simple floating-point loops.
  Fonenantsoa Maurica, Frédéric Mesnard and Étienne Payet.
• Bounded Abstract Interpretation.
  Maria Christakis and Valentin Wüstholz.
• Enforcing Termination of Interprocedural Analysis.
  Stefan Schulze Frielinghaus, Helmut Seidl and Ralf Vogler.

Friday, 9th of September, 2016, 9:00-10:00 : Invited Talk (Session Chair: Xavier Rival)

• Tom Henzinger :
  Quantitative Monitor Automata

Friday, 9th of September, 2016, 10:00-10:30 : Coffee Break

Friday, 9th of September, 2016, 10:30-12:00 : Verification (Session Chair: Jan Midtgaard)

• Automated Verification of Linearization Policies.
  Parosh Aziz Abdulla, Bengt Jonsson and Cong Quy Trinh.
• Cell morphing: from array programs to array-free Horn clauses.
  David Monniaux and Laure Gonnord.
• Relational Verification through Horn clause transformation.
  Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti.

Friday, 9th of September, 2016, 12:00-13:45 : Lunch

Friday, 9th of September, 2016, 13:45-14:00 : PC Chair Report

Friday, 9th of September, 2016, 14:00-15:00 : Invited Talk (Session Chair: Patrick Cousot)

• Jade Alglave :
  Simulation and Invariance for Weak Consistency

Friday, 9th of September, 2016, 15:00-15:30 : Weak Memory Models (Session Chair: Patrick Cousot)

• From array abstract domains to a parametric abstraction of concurrent programs under store-buffer-based relaxed memory models.
  Thibault Suzanne and Antoine Miné.

Friday, 9th of September, 2016, 18:00-22:00 : Visit and Banquet at Dynamic Earth

Saturday, 10th of September, 2016, 9:00-10:00 : Invited Talk (Session Chair: Xavier Rival)

• Fausto Spoto :
  The Julia Static Analyzer for Java

Saturday, 10th of September, 2016, 10:00-10:30 : Coffee Break

Saturday, 10th of September, 2016, 10:30-12:00 : Numeric Abstractions (Session Chair: Jérôme Feret)

• Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants.
  Pierre Roux, Yuen-Lam Voronin and Sriram Sankaranarayanan.
• Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis.
  Kensuke Kojima, Minoru Kinoshita and Kohei Suenaga.
• Exploiting sparsity in difference-bound matrices.
  Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard and Peter Stuckey.

Saturday, 10th of September, 2016, 12:00-14:00 : Lunch Break

Saturday, 10th of September, 2016, 14:00-15:00 : Transformation I (Session Chair: Roman Manevich)

• Completeness in Approximate Transduction.
  Mila Dalla Preda, Roberto Giacobazzi and Isabella Mastroeni.
• Securing A Compiler Transformation.
  Chaoqiang Deng and Kedar Namjoshi.

Saturday, 10th of September, 2016, 15:00-15:30 : Coffee Break

Saturday, 10th of September, 2016, 15:30-16:30 : Transformation II (Session Chair: Roman Manevich)

• Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM.
  David Menendez, Santosh Nagarakatte and Aarti Gupta.
• Loopy: Programmable and Formally Verified Loop Transformations.
  Kedar Namjoshi and Nimit Singhania.