SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Mon 18 Oct 2021 08:10 - 08:25 at Zurich B - Session 4B Chair(s): Antoine Miné
Mon 18 Oct 2021 16:10 - 16:25 at Zurich B - Session 4B Chair(s): Kedar Namjoshi

We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Miné’s approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Session 4BSAS at Zurich B
Chair(s): Antoine Miné Sorbonne Université
07:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
07:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
08:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
08:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
08:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS

15:40 - 17:00
Session 4BSAS at Zurich B -8h
Chair(s): Kedar Namjoshi Nokia Bell Labs
15:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
15:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
16:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
16:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
16:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS