Improving Thread-Modular Abstract Interpretation

Artifact for SAS '21 Paper: Improving Thread-Modular Abstract Interpretation 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. Please refer to sas21-artifact-description.md for the artifact descritption. For the most up-to-date version of the Goblint Static Analyzer, please refer to https://goblint.in.tum.deThis work was supported in part by Deutsche Forschungsgemeinschaft (DFG) – 378803395/2428 ConVeY and the Estonian Research Council grant PSG61