© 1991 by British Computer Society
Logic Programming for Software Verification and Testing
Syracuse University, P.O. Box 574, Syracuse, NY 13210-0574, USA
We propose a methodology for using logic programming to software verification and testing. The methodology is based on logic programming applications for the formation of decision-to-decision graph, path predicate evaluation and symbolic evaluation of output variables. We elaborate on an efficient software verification scheme which utilizes multiple dynamic theories in logic, organized as a tree structure. A technique to represent the symbolic environments as viewpoints of theories in logic, and an algorithm to locate the valid viewpoint of the leaf theories is presented. An Algol-like language is used to present our approach.
Received June 1989. revised June 1990.
* Syracuse University, P.O. Box 574, Syracuse, NY 13210-0574, USA