View in EDS PDF Full Text

Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.

Saved in:
Bibliographic Details
Title: Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.
Authors: Masaki Nakamura1, Kazuhiro Ogata2, Kokichi Futatsugi2
Source: International MultiConference of Engineers & Computer Scientists 2013. 2013, Vol. 1, p1-6. 6p.
Subjects: Rewriting systems (Computer science), Proof theory, Feature extraction, Programming languages, Object-oriented methods (Computer science), Computer software termination
Abstract: OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR]
Copyright of International MultiConference of Engineers & Computer Scientists 2013 is the property of International Association of Engineers (IAENG) 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: 97333874
AccessLevel: 6
PubType: Conference
PubTypeId: conference
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Masaki+Nakamura%22">Masaki Nakamura</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Kazuhiro+Ogata%22">Kazuhiro Ogata</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Kokichi+Futatsugi%22">Kokichi Futatsugi</searchLink><relatesTo>2</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22International+MultiConference+of+Engineers+%26+Computer+Scientists+2013%22">International MultiConference of Engineers & Computer Scientists 2013</searchLink>. 2013, Vol. 1, p1-6. 6p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Rewriting+systems+%28Computer+science%29%22">Rewriting systems (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Feature+extraction%22">Feature extraction</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Object-oriented+methods+%28Computer+science%29%22">Object-oriented methods (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of International MultiConference of Engineers & Computer Scientists 2013 is the property of International Association of Engineers (IAENG) 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=97333874
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 6
        StartPage: 1
    Subjects:
      – SubjectFull: Rewriting systems (Computer science)
        Type: general
      – SubjectFull: Proof theory
        Type: general
      – SubjectFull: Feature extraction
        Type: general
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Object-oriented methods (Computer science)
        Type: general
      – SubjectFull: Computer software termination
        Type: general
    Titles:
      – TitleFull: Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Masaki Nakamura
      – PersonEntity:
          Name:
            NameFull: Kazuhiro Ogata
      – PersonEntity:
          Name:
            NameFull: Kokichi Futatsugi
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Text: 2013
              Type: published
              Y: 2013
          Numbering:
            – Type: volume
              Value: 1
          Titles:
            – TitleFull: International MultiConference of Engineers & Computer Scientists 2013
              Type: main
ResultId 1