# Flow-Sensitive Composition of Thread-Modular Abstract Interpretation

arXiv: https://arxiv.org/abs/1709.10116 · HTML: https://mlsanity.com/paper/1709.10116/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2017.

## Built on by (most cited first, 2 of 2)

- [Certifying the Fairness of KNN in the Presence of Dataset Bias](https://mlsanity.com/paper/2307.08722/) (2023)
- [Systematic Testing of the Data-Poisoning Robustness of KNN](https://mlsanity.com/paper/2307.08288/) (2023)

## Abstract (arXiv)

We propose a constraint-based flow-sensitive static analysis for concurrent programs by iteratively composing thread-modular abstract interpreters via the use of a system of lightweight constraints. Our method is compositional in that it first applies sequential abstract interpreters to individual threads and then composes their results. It is flow-sensitive in that the causality ordering of interferences (flow of data from global writes to reads) is modeled by a system of constraints. These interference constraints are lightweight since they only refer to the execution order of program statements as opposed to their numerical properties: they can be decided efficiently using an off-the-shelf Datalog engine. Our new method has the advantage of being more accurate than existing, flow-insensitive, static analyzers while remaining scalable and providing the expected soundness and termination guarantees even for programs with unbounded data. We implemented our method and evaluated it on a large number of benchmarks, demonstrating its effectiveness at increasing the accuracy of thread-modular abstract interpretation.