Improving Thread-Modular Abstract Interpretation
Programming Languages
2021-08-18 v1
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'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.
Cite
@article{arxiv.2108.07613,
title = {Improving Thread-Modular Abstract Interpretation},
author = {Michael Schwarz and Simmo Saan and Helmut Seidl and Kalmer Apinis and Julian Erhard and Vesal Vojdani},
journal= {arXiv preprint arXiv:2108.07613},
year = {2021}
}
Comments
This is the extended version of a paper with the same title accepted at SAS'2021