A Translation-based Approach to the Verification of Modular Equivalence


Emilia Oikarinen and Tomi Janhunen. A translation-based approach to the verification of modular equivalence. Journal of Logic and Computation, 19(4):591–613, 2009.


The goal of this paper is to foster modular program development in answer set programming using a Gaifman-Shapiro-style module architecture. More specifically, a method for verifying the equivalence of logic program modules is devised and proved correct. The idea is to adapt a translation-based verification technique, which was originally devised for complete programs only, for program modules. In addition, optimization strategies are addressed in order to exploit the modular structure of programs in verification tasks. A number of experiments on verification strategies are also conducted using LPEQ which implements the verification method for the Smodels system. The preliminary experimental results reported in this paper suggest that the modularization of equivalence verification leads to potential time savings especially if the modules involved share a common context.

Suggested BibTeX entry:

    author = {Emilia Oikarinen and Tomi Janhunen},
    journal = {Journal of Logic and Computation},
    number = {4},
    pages = {591--613},
    title = {A Translation-based Approach to the Verification of Modular Equivalence},
    volume = {19},
    year = {2009},

This work is not available online here.