How to Transform an Analyzer into a Verifier
Marco Comini
Dipartimento di Matematica e Informatica, Università di Udine,
Via delle Scienze 206, 33100 Udine, Italy
comini-at-dimi.uniud.it
Roberta Gori and Giorgio Levi
Dipartimento di Informatica, Università di Pisa,
Corso Italia 40, 56125 Pisa, Italy
{gori, levi}-at-di.unipi.it
Abstract:
In this paper we push forward the idea of applying the abstract
interpretation concepts to the problem of verification of programs. We
consider the theory of abstract verification as proposed in
[CominiGLV99entcs,CominiGLV99] and we show how it is possible to transform
static analyzers with some suitable properties to obtain automatic
verification tools based on sufficient verification conditions. We prove
that the approach is general and flexible by showing three different
verification tools based on different domains of types for functional,
logic programming and CLP programming. The verifier for functional
programs is obtained from a static analyzer which implements one of the
polymorphic type domains introduced by Cousot [Cousot97c]. The one for
logic programs is obtained from a static analyzer on a type domain designed
by Codish and Lagoon [CodishL98], while the verifier for CLP programs is
obtained starting from the type analyzer described in [DrabentP98].
Marco Comini <comini-at-dimi.uniud.it>