Tabulation-based Induction Proofs with Application to Automated Verification

Abstract:

Tabled resolution methods introduce a new level of declarativeness over traditional (Prolog-like) logic programming systems. Availability of tabled LP systems makes it feasible to develop a larger class of efficient declarative solutions to complex applications. One such application is model checking, which is a verification technique aimed at determining whether a system specification possesses a certain property expressed as a temporal logic formula. From a computational viewpoint, algorithmic model checking can be formulated in terms of fixed-point computations. By encoding the semantics of process languages and temporal logics as logic programs we can cast this computation at a high level into computing the minimal model of the logic programs. By using metaprogramming facilities of logic programming, one can implement deductive techniques and thereby integrate them tightly with algorithmic model checking. In this abstract we illustrate how tabled resolution can be exploited to construct induction proofs.

Bibtex Entry:

@inproceedings{RRRS:TAPD98,
author = {Abhik Roychoudhury and  C. R. Ramakrishnan and  I. V. Ramakrishnan and  Scott A. Smolka},
title = {Tabulation-based Induction Proofs with Application to Automated Verification},
booktitle = {International Workshop on Tabulation in Parsing and Deduction ({TAPD})},
address = {Paris, France},
year = {1998}
}

Full Paper:

[pdf]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)