View Related Documents

Abstract

We study the application of abstract interpretation to the design of inductive methods for verifying properties of logic programs. We give a unified view of inductive assertion-based proof methods for logic programs, by systematically deriving them in a uniform way using Abstract Interpretation. The resulting verification framework allows us to reconstruct several existing verification methods and to understand the relation among them in terms of abstractions. Moreover, we can tackle the problem of establishing the completeness of the proof methods.

Keywords  Inductive proof methods - abstract interpretation - abstract domains

Fulltext Preview

Image of the first page of the fulltext document