Stratified Static Analysis Based on Variable Dependencies

TL;DR

This paper investigates the counterintuitive behavior of widening operators in static analysis, especially how analyzing subsets of variables can sometimes yield more precise results, and proposes simple solutions to address this issue.

Contribution

It introduces straightforward workarounds for the unexpected precision loss caused by certain widening operators in static analysis.

Findings

Analyzing variable subsets can sometimes improve precision.

Classical polyhedral widenings may behave unintuitively.

Proposed workarounds mitigate precision issues.

Abstract

In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening operators, including the classical one over finite polyhedra, exhibit an unintuitive behavior: analyzing the program over a subset of its variables may lead a more precise result than analyzing the original program! In this article, we present simple workarounds for such behavior.