Automated Verification of Behavioural Properties of Prolog Programs

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.