A Translation-based Approach to the Verification of Modular Equivalence

Reference:

Emilia Oikarinen and Tomi Janhunen. A translation-based approach to the verification of modular equivalence. In Stefania Costantini and Richard Watson, editors, Proceedings of the 4th Workshop on Answer Set Programming; Advances in Theory and Implementation (ASP 2007), pages 255–269, Porto, Portugal, September 2007.

Abstract:

In this paper, a method for verifying the equivalence of logic program modules under a Gaifman-Shapiro-style module architecture is proposed. 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. Preliminary results indicate that at least in certain cases the overall time spent on verification tasks can be reduced through modularization.

Suggested BibTeX entry:

@inproceedings{OJ07:asp,
    address = {Porto, Portugal},
    author = {Emilia Oikarinen and Tomi Janhunen},
    booktitle = {Proceedings of the 4th Workshop on Answer Set Programming; Advances in Theory and Implementation (ASP 2007)},
    editor = {Stefania Costantini and Richard Watson},
    month = {September},
    pages = {255-269},
    title = {A Translation-based Approach to the Verification of Modular Equivalence},
    year = {2007},
}

See www.tcs.hut.fi ...