Program verification system with synthesizer of invariant assertions

Seiichiro Dan, Takahira Yamaguchi, Osamu Kakusho, Yoshikazu Tezuka

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

The authors describe the implementation of an automatic program verification system using a synthesizer of invariant assertions. This comprehensive system inputs the program, obtains specifications (invariant assertion generation), generates verification conditions, and proves the verification conditions. The system is regarded as more realistic and promising than existing program verification systems.

Original languageEnglish
Pages (from-to)1-13
Number of pages13
JournalSystems and Computers in Japan
Volume20
Issue number1
Publication statusPublished - 1989 Jan
Externally publishedYes

Fingerprint

Program Verification
Assertion
Invariant
Automatic Verification
Specification
Specifications

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Hardware and Architecture
  • Information Systems
  • Theoretical Computer Science

Cite this

Program verification system with synthesizer of invariant assertions. / Dan, Seiichiro; Yamaguchi, Takahira; Kakusho, Osamu; Tezuka, Yoshikazu.

In: Systems and Computers in Japan, Vol. 20, No. 1, 01.1989, p. 1-13.

Research output: Contribution to journalArticle

Dan, Seiichiro ; Yamaguchi, Takahira ; Kakusho, Osamu ; Tezuka, Yoshikazu. / Program verification system with synthesizer of invariant assertions. In: Systems and Computers in Japan. 1989 ; Vol. 20, No. 1. pp. 1-13.
@article{059bc593460c42699e098037d47f992b,
title = "Program verification system with synthesizer of invariant assertions",
abstract = "The authors describe the implementation of an automatic program verification system using a synthesizer of invariant assertions. This comprehensive system inputs the program, obtains specifications (invariant assertion generation), generates verification conditions, and proves the verification conditions. The system is regarded as more realistic and promising than existing program verification systems.",
author = "Seiichiro Dan and Takahira Yamaguchi and Osamu Kakusho and Yoshikazu Tezuka",
year = "1989",
month = "1",
language = "English",
volume = "20",
pages = "1--13",
journal = "Systems and Computers in Japan",
issn = "0882-1666",
publisher = "John Wiley and Sons Inc.",
number = "1",

}

TY - JOUR

T1 - Program verification system with synthesizer of invariant assertions

AU - Dan, Seiichiro

AU - Yamaguchi, Takahira

AU - Kakusho, Osamu

AU - Tezuka, Yoshikazu

PY - 1989/1

Y1 - 1989/1

N2 - The authors describe the implementation of an automatic program verification system using a synthesizer of invariant assertions. This comprehensive system inputs the program, obtains specifications (invariant assertion generation), generates verification conditions, and proves the verification conditions. The system is regarded as more realistic and promising than existing program verification systems.

AB - The authors describe the implementation of an automatic program verification system using a synthesizer of invariant assertions. This comprehensive system inputs the program, obtains specifications (invariant assertion generation), generates verification conditions, and proves the verification conditions. The system is regarded as more realistic and promising than existing program verification systems.

UR - http://www.scopus.com/inward/record.url?scp=0024304290&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024304290&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0024304290

VL - 20

SP - 1

EP - 13

JO - Systems and Computers in Japan

JF - Systems and Computers in Japan

SN - 0882-1666

IS - 1

ER -