Abstract interpretation based verification of logic programs

This paper is an overview of our results on the application of abstract interpretation concepts to various problems related to the verification of logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains. We derive an assertion based verification method and we show two instances based on different assertion languages: a decidable assertion language and CLP used as an assertion language.