Improving Thread-Modular Abstract Interpretation

TL;DR

This paper introduces a generalized thread-modular abstract interpretation framework that unifies and improves upon existing static analysis techniques, with experimental validation on benchmark suites.

Contribution

It formalizes thread-modular analyses using global invariants and constraint systems, unifies existing approaches, and offers a refined analysis with enhanced precision.

Findings

The generalized framework encompasses Goblint and Miné's approaches.

The refined analysis improves precision over individual methods.

Experimental results demonstrate the effectiveness of the proposed analysis.

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.