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

Abstract. We propose a novel approach for computing weakest liberal safe pre-conditions 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 decom-position 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 subtrac-tion operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not re-stricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures.