Principles of proof scores in CafeOBJ

Kokichi Futatsugi, Daniel Gaina, Kazuhiro Ogata

Research output: Contribution to journalArticle

22 Citations (Scopus)

Abstract

This paper describes the theoretical principles of a verification method with proof scores in the CafeOBJ algebraic specification language. The verification method focuses on specifications with conditional equations and realizes systematic theorem proving (or interactive verification). The method is explained using a simple but instructive example, and the necessary theoretical foundations, which justify every step of the verification, are described with precise mathematical definitions. Some important theorems that result from the definitions are also presented.

Original languageEnglish
Pages (from-to)90-112
Number of pages23
JournalTheoretical Computer Science
Volume464
DOIs
Publication statusPublished - Dec 14 2012
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Principles of proof scores in CafeOBJ'. Together they form a unique fingerprint.

  • Cite this