VeriPolyTypes: a tool for Verification of Logic Programs w.r.t. Type Specifications

Marco Comini
Dipartimento di Matematica e Informatica, Università di Udine,
Via delle Scienze 206, 33100 Udine, Italy
comini-at-dimi.uniud.it

Abstract:

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