Propagation: A New Operation in a Framework for Abstract Interpretation of Logic Programs

ract Interpretation of Logic Programs Maurice Bruynooghe and Gerda :Ianssens Department of Computer Science, Katholleke Universiteit Leuven Celestijnenlaan 200A, B-3001 Heverlee, Belgium e-maih {maurice,gerda}Ocs.kuleuven.ac.be Abstract. Most frameworks for abstract interpretation of logic programs provide abstract operations which safely approximate their concrete counterpart. That means, given a concrete state ,.qdescribed by an abstract state AS and a concrete operation 0 producing 0(5), the correabstract 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 propagap which reexecutes - at the abstract level - all operations leading until a stable abstract state is reached. We illustrate the novel framework with a mode analysis which, notwithstanding a very simple domain, reaches on several examples similar precision as mode systems using much complexer abstr...

• Type: Conference
• Year: 1992
• Where: META
• Authors: Maurice Bruynooghe, Gerda Janssens
• Keywords: Abstract State, Automated Reasoning, E-maih {maurice, Gerda}ocs.kuleuven.ac.be Abstract, META 1992