Marco Comini
Dipartimento di Matematica e Informatica, Università di Udine,
Via delle Scienze 206, 33100 Udine, Italy
comini-at-dimi.uniud.it
This work concerns 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.
This verifier uses three verification methods over the types domain developed
by M.Codish and V.Lagoon. The code of our verifier is based on the existing
abstract operations defined in the implementation of Lagoon.
A more extended description is in this
paper
Keywords: Logic Programming, Declarative diagnosis, Verification, Semantics, Debugging.