Marco Comini
Dipartimento di Matematica e Informatica, Università di Udine,
Via delle Scienze 206, 33100 Udine, Italy
comini-at-dimi.uniud.it
In this system demonstration we present a tool for the verification of Logic Programs w.r.t. type information specifications. The tool is based on sufficient verification conditions obtained by abstract interpretation.
Following the theoretical foundation in [CominiGL01,CominiGLV99entcs,CominiGLV99], the tool is obtained by transforming a static analyzer on a type domain for Logic Programs designed by Codish and Lagoon [CodishL98].
More on the Tool Sources