Program analysis with local policy iteration

DOI10.1007/978-3-662-49122-5_6MaRDI QIDQ2796041zbMATH OpenOpenAlexFDO

Authors Egor George Karpenkov, David Monniaux, Philipp Wendler

Publication date 23 March 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1509.03424

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Static Analysis by Policy Iteration on Relational Domains
• Policy iteration in finite templates domain
• Computer Aided Verification
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Integrating Policy Iterations in Abstract Interpreters

Cited in

(5)

• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Integrating Policy Iterations in Abstract Interpreters
• Computer Aided Verification
• Fast numerical program analysis with reinforcement learning
• A change-based heuristic for static analysis with policy iteration

Describes a project that uses

Uses Software

• BLAST
• CPAchecker
• PAGAI

This page was built for publication: Program analysis with local policy iteration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2796041)