School of Computing

Forward versus Backward Verification of Logic Programs

Andy King and Lunjin Lu

Technical Report 5-03, University of Kent, Computing Laboratory, University of Kent, April 2003.

Abstract

One recent development in logic programming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify that the assertions hold. The dual approach is apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. This paper is a systematic comparison of these two approaches to verification. The paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.

Download publication 426 kbytes (PostScript)

Bibtex Record

@techreport{1618,
author = {Andy King and Lunjin Lu},
title = {Forward versus {B}ackward {V}erification of {L}ogic {P}rograms},
month = {April},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/1618},
    publication_type = {techreport},
    submission_id = {25881_1053502050},
    number = {5-03},
    address = {University of Kent},
    institution = {University of Kent, Computing Laboratory},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014