Helmut Seidl

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 warro...