SAS 2010 Advanced Program

Tuesday, September 14, 2010

9:00-10:00 Welcome and Invited Talk (Chair: Neil Jones)

Manuel Fahndrich, Microsoft Research, USA, Static Verification for Code Contracts

Coffee Break

10:30-12h10 Session 1 (Chair: Elvira Albert)

Azadeh Farzan and Zachary Kincaid. Compositional Bitvector Analysis for Concurrent Programs with Nested Locks

Alexander Malkis, Andreas Podelski and Andrey Rybalchenko. Thread-Modular Counterexample-Guided Abstraction Refinement

Christian J. Bell, David Walker and Andrew Appel. Concurrent Separation Logic for Pipelined Parallelization

Martin Vechev, Eran Yahav, Raghavan Raman and Vivek Sarkar. Verifying Determinism of Structured Parallel Programs

Lunch Break

14:00-15:15 Session 2 (Chair: Dave Schmidt)

Christophe Alias, Alain Darte, Paul Feautrier and Laure Gonnord. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

William Harris, Akash Lal, Aditya Nori and Sriram Rajamani. Alternation for Termination

Tom Schrijvers and Alan Mycroft. Strictness Meets Data Flow

Coffee Break

15:45-18:15 Special Session in Memory of Robin Milner and Amir Pnueli
(Chair: Patrick Cousot)

James Leifer, INRIA, France

E. Allen Emerson, The University of Texas at Austin, USA

Joachim Parrow, Uppsala Universitet, Sweden

Benjamin Goldberg, New York University, USA

Glynn Winskel, University of Cambridge, UK

Wednesday, September 15, 2010

9:00-10:00 Invited Talk (Chair: Radhia Cousot)

Mooly Sagiv, Tel-Aviv University, Israel, Statically Inferring Complex Heap, Array, and Numeric Invariants

Coffee Break

10:30-12:10 Session 3 (Chair: Damien Massé)

Joerg Brauer and Andy King. Automatic Abstraction for Intervals using Boolean Formulae

Thomas Martin Gawlitza and Helmut Seidl. Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones precisely

Gianluca Amato, Francesca Scozzari and Maurizio Parton. Deriving numerical abstract domains via Principal Component Analysis

Alexandre Chapoutot. Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables

Lunch Break

14:00-15:15 Session 4 (Chair: Roberto Giacobazzi)

Simon Holm Jensen, Anders Møller and Peter Thiemann. Interprocedural Analysis with Lazy Propagation

Elvira Albert, Puri Arenas, Samir Genaim, German Puebla and Diana Vanessa Ramírez Deantes. From Object Fields to Local Variables: a Practical Approach to Field-Sensitive Analysis

Matthew Might. Abstract interpreters for free

15:30-19:30 Excursion (Guided tour of Collioure)

20:30 Conference Diner at Domaine de Rombeau

Thursday, September 16, 2010

9:00-10:00 Invited Talk (Chair: Matthieu Martel)

David Lesens, EADS Space Transportation, France, Using Static Analysis in Space: Why doing so?

Coffee Break

10:30-12:10 Session 5 (Chair: Matt Might)

Larissa Meinicke, Annabelle McIver, Carroll Morgan and Joost-Pieter Katoen. Linear-invariant generation for probabilistic programs

Aleksandr Karbyshev, Helmut Seidl and Martin Hofmann. Verifying a Local Generic Solver in Coq

Isil Dillig, Thomas Dillig and Alex Aiken. Small Formulas for Large Programs: On-line Constraint Simplification in Scalable Static Analysis

Rupesh Nasre and Ramaswamy Govindarajan. Points-to Analysis as a System of Linear Equations

Lunch Break

14:00-15:00 Invited Talk (Chair: Manuel Hermenegildo)

Andreas Podelski, Freiburg University, Germany, Size-Change Termination and Transition Invariants

Coffee Break

15:30-17:15 Session 6 (Chair: Laurent Mauborgne)

Mila Dalla Preda, Roberto Giacobazzi, Saumya Debray, Kevin Coogan and Gregg M. Townsend. Modelling Metamorphism by Abstract Interpretation

Arie Gurfinkel and Sagar Chaki. BOXES: A Symbolic Abstract Domain of Boxes

Nadir Matringe, Arnaldo Moura and Rachid Rebiha. Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods

Renato Cherini, Lucas Rearte and Javier Blanco. A Shape Analysis for Non-linear Data Structures

Concluding Remarks