@inproceedings{dd370f40ace64bc6af9e48731183001d,
title = "Improving Thread-Modular Abstract Interpretation",
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{\'e}{\textquoteright}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.",
keywords = "Collecting trace semantics, Concurrent systems, Global invariants, Side-effects, Thread-modular abstract interpretation",
author = "Michael Schwarz and Simmo Saan and Helmut Seidl and Kalmer Apinis and Julian Erhard and Vesal Vojdani",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 28th International Symposium on Static Analysis, SAS 2021 ; Conference date: 17-10-2021 Through 19-10-2021",
year = "2021",
doi = "10.1007/978-3-030-88806-0_18",
language = "English",
isbn = "9783030888053",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "359--383",
editor = "Cezara Dr{\u a}goi and Suvam Mukherjee and Kedar Namjoshi",
booktitle = "Static Analysis - 28th International Symposium, SAS 2021, Proceedings",
}