Modular Verification of Logic Programs

Recentely, a new approach to verification of logic and Prolog programs has been proposed, whose main advantage is the possibility to reason on different properties in a unified framework. In this paper, we show an equivalent formulation of that proof method which is well-suited for modular program verification. The notion of modularity taken into account is based on stratification. We show that the proofs of correctness of a program P and a program Q can be re-used in the proof of correctness of P "union" Q with small additional efforts. The main advantage consists in the fact that the proofs for P and Q are developed in a fully independent way.