Tuesday, August 28th

09:00 - 17:00

Workshop Day

SASB 2018

TAPAS 2018

18:00

Welcome Reception

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

14:30 - 15:00

Coffee Break

17:00

Food and Wine Tour