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

Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.

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