Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

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

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

4 Scopus citations

Abstract

We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings
EditorsThomas Wies
PublisherSpringer Science and Business Media Deutschland GmbH
Pages28-58
Number of pages31
ISBN (Print)9783031300431
DOIs
StatePublished - 2023
Event32nd European Symposium on Programming, ESOP 2023, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023 - Paris, France
Duration: 22 Apr 202327 Apr 2023

Publication series

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

Conference

Conference32nd European Symposium on Programming, ESOP 2023, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023
Country/TerritoryFrance
CityParis
Period22/04/2327/04/23

Keywords

  • clusters
  • collecting local trace semantics
  • concurrency
  • dynamic thread creation
  • thread-modular relational abstract interpretation

Fingerprint

Dive into the research topics of 'Clustered Relational Thread-Modular Abstract Interpretation with Local Traces'. Together they form a unique fingerprint.

Cite this