Improving Thread-Modular Abstract Interpretation

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

9 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationStatic Analysis - 28th International Symposium, SAS 2021, Proceedings
EditorsCezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi
PublisherSpringer Science and Business Media Deutschland GmbH
Pages359-383
Number of pages25
ISBN (Print)9783030888053
DOIs
StatePublished - 2021
Event28th International Symposium on Static Analysis, SAS 2021 - Chicago, United States
Duration: 17 Oct 202119 Oct 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12913 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th International Symposium on Static Analysis, SAS 2021
Country/TerritoryUnited States
CityChicago
Period17/10/2119/10/21

Keywords

  • Collecting trace semantics
  • Concurrent systems
  • Global invariants
  • Side-effects
  • Thread-modular abstract interpretation

Fingerprint

Dive into the research topics of 'Improving Thread-Modular Abstract Interpretation'. Together they form a unique fingerprint.

Cite this