Specification-based Automatic Verification of Prolog Programs

The paper presents an analyzer for verifying the correctness of a Prolog program relative to a specification which provides a list of input/output annotations for the arguments and parameters that can be used to establish program termination. The work stems from Deville's methodology to derive Prolog programs that correctly implement their declarative meaning. In this context, we propose an algorithm that combines, adapts, and sometimes improves various existing static analyses in order to verify total correctness of Prolog programs with respect to formal specifications. Using the information computed during the verification process, an automatic complexity analysis can be also performed