Flow-sensitive and flow-insensitive analyses of programs occupy opposite ends of a spectrum. Between these extremes lie mixed flow sensitive approaches, where some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the analysis of multi-threaded code or code withnon-local control flow. Another instance is global store widening for efficient analysis of functional languages and some forms of pointer analysis. While mixed flow-sensitive analyses are common in the literature, the formulation of the particular analysis problem and the means to solve it are often tightly coupled. Side-effecting constraint systems provide a generic mechanism for describing mixed flow-sensitive analyses, thus decoupling the analysis definition from solver algorithm details. The abstract interpreter Goblint realizes this decoupling, and allows defining mixed flow-sensitive analyses independently of generic solvers. We indicate how the precision of specified analyses can be improved using digests (on the side of the formulation of the analysis problem) and suitable update rules (on the side of the solver). We explain how developers can use Goblint to implement their own mixed flow-sensitive analyses.
Formal Methods (FM)
2026-05-18
2026-06-24