Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
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 OctDisplayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | 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 15mTalk | Backward Symbolic Execution with Loop FoldingVirtual SAS | ||
08:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4B Discussion, Questions and Answers SAS |
15:40 - 17:00 | |||
15:40 15mTalk | 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 15mTalk | Backward Symbolic Execution with Loop FoldingVirtual SAS | ||
16:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4B Discussion, Questions and Answers SAS |