Logic Programming for Software Verification and Testing
Sanjeev Khanna · The Computer Journal · 1991
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.