Proving Total Correctness of Top-Down Solvers with Widening and Narrowing

Abstract

The top-down solver TD is a generic fixpoint algorithm that can be used to compute partial post-solutions of equation systems for abstract interpretation. We consider two extensions of the TD to deal with infinite strictly ascending chains. For the TD extended with warrowing, we formally prove that it always returns partial post-solutions, while for the TD extended with widening and narrowing in phases, we prove termination provided that the set of unknowns is finite. By proving the equivalence of the two extensions, we deduce the total correctness of both solvers. For the equivalence to hold, we in particular assume the equation system to have right-hand sides that are both monotonic and have monotonic dependencies. We demonstrate with counterexamples that the violation of any of the assumptions may compromise the equivalence. All proofs have been formalized using the interactive theorem prover Isabelle.