View in EDS PDF Full Text

A Translation-based Approach to the Verification of Modular Equivalence.

Saved in:
Bibliographic Details
Title: A Translation-based Approach to the Verification of Modular Equivalence.
Authors: OIKARINEN, EMILIA1 Emilia.Oikarinen@tkk.fi, JANHUNEN, TOMI1 Tomi.Janhunen@tkk.fi
Source: Journal of Logic & Computation. Aug2009, Vol. 19 Issue 4, p591-613. 23p. 3 Black and White Photographs, 5 Charts.
Subjects: Modular programming, Computer programming, Computer architecture, Logic programming, Computer software
Abstract: The goal of this article 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 article suggest that the modularization of equivalence verification leads to potential time savings especially if the modules involved share a common context. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 45280333
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A Translation-based Approach to the Verification of Modular Equivalence.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22OIKARINEN%2C+EMILIA%22">OIKARINEN, EMILIA</searchLink><relatesTo>1</relatesTo><i> Emilia.Oikarinen@tkk.fi</i><br /><searchLink fieldCode="AR" term="%22JANHUNEN%2C+TOMI%22">JANHUNEN, TOMI</searchLink><relatesTo>1</relatesTo><i> Tomi.Janhunen@tkk.fi</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Aug2009, Vol. 19 Issue 4, p591-613. 23p. 3 Black and White Photographs, 5 Charts.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Modular+programming%22">Modular programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+programming%22">Computer programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+architecture%22">Computer architecture</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+programming%22">Logic programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: The goal of this article 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 article suggest that the modularization of equivalence verification leads to potential time savings especially if the modules involved share a common context. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=45280333
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1093/logcom/exn039
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 23
        StartPage: 591
    Subjects:
      – SubjectFull: Modular programming
        Type: general
      – SubjectFull: Computer programming
        Type: general
      – SubjectFull: Computer architecture
        Type: general
      – SubjectFull: Logic programming
        Type: general
      – SubjectFull: Computer software
        Type: general
    Titles:
      – TitleFull: A Translation-based Approach to the Verification of Modular Equivalence.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: OIKARINEN, EMILIA
      – PersonEntity:
          Name:
            NameFull: JANHUNEN, TOMI
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2009
              Type: published
              Y: 2009
          Identifiers:
            – Type: issn-print
              Value: 0955792X
          Numbering:
            – Type: volume
              Value: 19
            – Type: issue
              Value: 4
          Titles:
            – TitleFull: Journal of Logic & Computation
              Type: main
ResultId 1