PROPAGATION - A NEW OPERATION IN A FRAMEWORK FOR ABSTRACT INTERPRETATION OF LOGIC PROGRAMS

Most frameworks for abstract interpretation of logic programs provide abstract operations which safely approximate their concrete counterpart. That means, given a concrete state S described by an abstract state AS and a concrete operation O producing O(S), the corresponding abstract operation AO produces AO(AS) which must describe O(S). We sketch a framework which relaxes this condition and requires that the safe approximation condition is only reached after a propagation step which reexecutes - at the abstract level - all operations leading to O(S) until a stable abstract state is reached. We illustrate the novel framework with a mode analysis which, notwithstanding a very simple abstract domain, reaches on several examples similar precision as mode analysis systems using much complexer abstract domains.