Program Analysis with Local Policy Iteration

TL;DR

This paper introduces a novel program analysis algorithm that combines the accuracy of max-policy iteration with the scalability of Kleene iterations, integrated within the CPA framework for effective numerical invariant derivation.

Contribution

It presents a new algorithm for numerical invariant analysis that operates over template linear domains and can be integrated with existing analysis frameworks.

Findings

Favorable performance on SV-Comp benchmarks.

Operates efficiently over various template linear domains.

Combines precision of max-policy iteration with scalability of Kleene iterations.

Abstract

We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication. It uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source. The implementation is evaluated on a set of benchmarks from the Software Verification Competition (SV-Comp). It competes favorably with state-of-the-art analyzers.