n 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 and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic Verification tools based on suficient verification conditions. We prove that the approach is general and flexible by showing three difierent Verification tools based on difierent domains of types for functional, logic 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. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon, while the verifier for CLP programs is obtained from the type analyzer described in [15].

How to Transform an Analyzer into a Verifier

GORI, ROBERTA;
2001

Abstract

n 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 and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic Verification tools based on suficient verification conditions. We prove that the approach is general and flexible by showing three difierent Verification tools based on difierent domains of types for functional, logic 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. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon, while the verifier for CLP programs is obtained from the type analyzer described in [15].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/191862
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact