25th Static Analysis Symposium
August 29th - August 31st, 2018, Freiburg im Breisgau, Germany

Program


Tuesday, August 28th


Workshop Day


Wednesday, August 29th


09:00 - 10:00

Invited Talk


Fairness: A Formal-Methods Perspective
Aws Albarghouthi


10:00 - 10:30

Coffee Break


10:30 - 12:00

Session 1

Modular Software Fault Isolation as Abstract Interpretation

Frédéric Besson, Thomas Jensen and Julien Lepiller

A Reduced Product of Absolute and Relative Error Bounds for Floating-point Analysis

Maxime Jacquemin, Sylvie Putot and Franck Védrine

Invertible Linear Transforms of Numerical Abstract Domains

Francesco Ranzato and Marco Zanella


12:30 - 13:30

Lunch


13:30 - 14:30

Invited Talk


New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair
Ruzica Piskac


14:30 - 15:00

Coffee Break


15:00 - 16:30

Session 2

Block-Size Independence for GPU Programs

Rajeev Alur, Joseph Devietti and Nimit Singhania

The Impact of Program Transformations on Static Program Analysis

Kedar Namjoshi and Zvonimir Pavlinovic

Abstract Interpretation of Stateful Networks

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham and Yaron Velner


16:30 - 17:00

Coffee Break


17:00 - 18:00

Invited Tutorial


The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software
Roberto Bagnara


18:30

Reception and Banquet

Schlossbergrestaurant Dattler
(10 min walk from the conference venue)


Thursday, August 30th


09:00 - 10:00

Invited Talk


Interactive Verification of Distributed Protocols Using Decidable Logic
Sharon Shoham


10:00 - 10:30

Coffee Break


10:30 - 12:00

Session 3

Volume-Based Merge Heuristics for Disjunctive Numeric Domains

Andrew Ruef, Kesha Hietala and Arlen Cox

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints

Alexey Bakhirkin and David Monniaux

Verifying Bounded Subset-Closed Hyperproperties

Isabella Mastroeni and Michele Pasqua


12:00 - 13:30

Lunch


13:30 - 15:00

Session 4


Efficiently Learning Safety Proofs from Appearance as well as Behaviours

Sumanth Prabhu, Kumar Madhukar and Venkatesh R.

Abstract Interpretation of CTL Properties

Caterina Urban, Samuel Ueltschi and Peter Müller

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

Anna Becchi and Enea Zaffanella


15:00 - 15:30

Coffee Break


15:30 - 17:00

Session 5

Process-Local Static Analysis of Synchronous Processes

Jan Midtgaard, Flemming Nielson and Hanne Riis Nielson

Modular Static Analysis of String Manipulations in C Programs

Matthieu Journault, Antoine Miné and Abdelraouf Ouadjaout

Closing the Performance Gap between Doubles and Rationals for Octagons

Aziem Chawdhary and Andy King


17:00 - 17:30

Coffee Break


17:30 - 18:30

Invited Tutorial


Deductive Verification in Decidable Fragments with Ivy
Kenneth L. McMillan and Oded Padon


Friday, August 31st


09:00 - 10:00

Invited Talk

Numerical Invariants via Abstract Machines

Zachary Kincaid


10:00 - 10:30

Coffee Break


10:30 - 12:00

Session 6

Verifying Properties of Differentiable Programs

Jan Hueckelheim, Ziqing Luo, Sri Hari Krishna Narayanan, Stephen F. Siegel and Paul Hovland

Incremental Verification Using Trace Abstraction

Bat-Chen Rothenberg, Daniel Dietsch and Matthias Heizmann
Inductive Termination Proofs with Transition Invariants and their relationship to the Size-Change Abstraction

Florian Zuleger


12:00 - 13:30

Lunch


13:30 - 14:30

Invited Tutorial


Experience Developing and Deploying Concurrency Analysis at Facebook
Peter O'Hearn


19:00

Food and Wine Tour