SPLASH 2021 (series) / SAS 2021 (series) / SAS 2021 - 28th Static Analysis Symposium / Improving Thread-Modular Abstract Interpretation
Improving Thread-Modular Abstract InterpretationVirtual
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
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 OctDisplayed time zone: Central Time (US & Canada) change
Mon 18 Oct
Displayed 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 |