Program verification is a crucial issue in the field of program development, compilation and debugging. In this paper, we present an analyser for Prolog which aims at verifying whether the execution of a program behaves according to a given specification (behavioural assumptions). The analyser is based on the methodology of abstract interpretation. A novel notion of abstract sequence is introduced, that includes an over- approximatimation of successful inputs (this is useful to detect mutual exclusion of clauses, and expresses size relation information between successful inputs and the corresponding outputs, together with cardinality information in terms of input argument sizes.
Automated Verification of Behavioural Properties of Prolog Programs
ROSSI, Sabina;CORTESI, Agostino
1997-01-01
Abstract
Program verification is a crucial issue in the field of program development, compilation and debugging. In this paper, we present an analyser for Prolog which aims at verifying whether the execution of a program behaves according to a given specification (behavioural assumptions). The analyser is based on the methodology of abstract interpretation. A novel notion of abstract sequence is introduced, that includes an over- approximatimation of successful inputs (this is useful to detect mutual exclusion of clauses, and expresses size relation information between successful inputs and the corresponding outputs, together with cardinality information in terms of input argument sizes.File | Dimensione | Formato | |
---|---|---|---|
asian97.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
Accesso chiuso-personale
Dimensione
214.67 kB
Formato
Adobe PDF
|
214.67 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.