language: en

Proving Properties of Logic Programs by Abstract Diagnosis

Marco Comini , Giorgio Levi , Maria Chiara Meo , and Giuliana Vitiello
Dipartimento di Informatica, Universita di Pisa,
Corso Italia 40, 56125 Pisa, Italy,
{comini, levi}@di.unipi.it
Dipartimento di Matematica Pura ed Applicata, Universit`a di LAquila,
via Vetoio, localit`a Coppito, 67010 LAquila, Italy,
meo@univaq.it
Dipartimento di Informatica ed Applicazioni, Universit`a di Salerno,
Baronissi (Salerno), Italy,
giuvit@dia.unisa.it

Abstract. We show how declarative diagnosis techniques can be extended to cope with verification of operational properties, such as computed answers, and of abstract properties, such as types and groundness dependencies. The extension is achieved by using a simple semantic framework, based on abstract interpretation. The resulting technique (abstract diagnosis) leads to elegant bottom-up and top-down verification methods, which do not require to determine the symptoms in advance, and which are effective in the case of abstract properties described by finite domains.

Keywords: Logic Programming, Declarative diagnosis, Verification, Semantics, Debugging