Logic programs as specifications in the inductive verification of logic programs
Marco Comini, Roberta Gori, Giorgio Levi · Electronic Notes in Theoretical Computer Science · 2001
In this paper we define a new verification method based on an assertion language able to express properties defined by the user through a logic program. We first apply the verification framework defined in [3] to derive sufficient inductive conditions to prove partial correctness. Then we show how the resulting conditions can be proved using program transformation techniques.