SAS 2016 Accepted Papers

Kedar Namjoshi and Nimit Singhania. Loopy: Programmable and Formally Verified Loop Transformations
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard and Peter Stuckey. Exploiting sparsity in difference-bound matrices
Kihong Heo, Hakjoo Oh and Hongseok Yang. Learning a Variable-Clustering Strategy for Octagon From Labeled Data Generated by a Static Analysis
David Monniaux and Laure Gonnord. Cell morphing: from array programs to array-free Horn clauses
George Balatsouras and Yannis Smaragdakis. Structure-Sensitive Points-To Analysis for C and C++
David Menendez, Santosh Nagarakatte and Aarti Gupta. Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
Francesco Ranzato. Abstract Interpretation of Supermodular Games
Mila Dalla Preda, Roberto Giacobazzi and Isabella Mastroeni. Completeness in Approximate Transduction
Fonenantsoa Maurica, Frédéric Mesnard and Étienne Payet. On the linear ranking problem for simple floating-point loops
Tian Tan, Yue Li and Jingling Xue. Making k-Object-Sensitive Pointer Analysis More Precise with Still k-Limiting
Stefan Schulze Frielinghaus, Helmut Seidl and Ralf Vogler. Enforcing Termination of Interprocedural Analysis
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Relational Verification through Horn clause transformation
Jan Midtgaard, Flemming Nielson and Hanne Riis Nielson. An Abstract Domain Functor for Lattice-Valued Regular Expressions
Pritam Gharat, Uday Khedker and Alan Mycroft. Flow and Context Sensitive Points-to Analysis using Generalized Points-to Graphs
Thibault Suzanne and Antoine Miné. From array abstract domains to a parametric abstraction of concurrent programs under store-buffer-based relaxed memory models
Maria Christakis and Valentin Wüstholz. Bounded Abstract Interpretation
Kensuke Kojima, Minoru Kinoshita and Kohei Suenaga. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
Matthieu Journault and Antoine Miné. Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Program
Parosh Aziz Abdulla, Bengt Jonsson and Cong Quy Trinh. Automated Verification of Linearization Policies
Pierre Roux, Yuen-Lam Voronin and Sriram Sankaranarayanan. Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants
Chaoqiang Deng and Kedar Namjoshi. Securing A Compiler Transformation