Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction

Alexey Bakhirkin, Josh Berdine, and Nir Piterman

Abstract

We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either under-approximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using over-approximation, while in order to maintain soundness we use an under-approximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures.

Details

Publication typeTechReport
NumberMSR-TR-2014-82
PublisherMicrosoft Research
> Publications > Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction