Program Analysis with Local Policy Iteration

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