A lightweight integration of theorem proving and model checking for system verification

Weiqiang Kong, Kazuhiro Ogata, Takahiro Seino, Kokichi Futatsugi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Citations (Scopus)

Abstract

Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs " in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.

Original languageEnglish
Title of host publicationProceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05
Pages59-66
Number of pages8
DOIs
Publication statusPublished - Dec 1 2005
Event12th Asia-Pacific Software Engineering Conference, APSEC'05 - Taipei, Taiwan, Province of China
Duration: Dec 15 2005Dec 17 2005

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume2005
ISSN (Print)1530-1362

Other

Other12th Asia-Pacific Software Engineering Conference, APSEC'05
CountryTaiwan, Province of China
CityTaipei
Period12/15/0512/17/05

Fingerprint

Theorem proving
Model checking
Specifications

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Kong, W., Ogata, K., Seino, T., & Futatsugi, K. (2005). A lightweight integration of theorem proving and model checking for system verification. In Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05 (pp. 59-66). [1607137] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 2005). https://doi.org/10.1109/APSEC.2005.9

A lightweight integration of theorem proving and model checking for system verification. / Kong, Weiqiang; Ogata, Kazuhiro; Seino, Takahiro; Futatsugi, Kokichi.

Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05. 2005. p. 59-66 1607137 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 2005).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kong, W, Ogata, K, Seino, T & Futatsugi, K 2005, A lightweight integration of theorem proving and model checking for system verification. in Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05., 1607137, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, vol. 2005, pp. 59-66, 12th Asia-Pacific Software Engineering Conference, APSEC'05, Taipei, Taiwan, Province of China, 12/15/05. https://doi.org/10.1109/APSEC.2005.9
Kong W, Ogata K, Seino T, Futatsugi K. A lightweight integration of theorem proving and model checking for system verification. In Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05. 2005. p. 59-66. 1607137. (Proceedings - Asia-Pacific Software Engineering Conference, APSEC). https://doi.org/10.1109/APSEC.2005.9
Kong, Weiqiang ; Ogata, Kazuhiro ; Seino, Takahiro ; Futatsugi, Kokichi. / A lightweight integration of theorem proving and model checking for system verification. Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05. 2005. pp. 59-66 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC).
@inproceedings{43773be8acbf4b06967c2e96b7ddfe71,
title = "A lightweight integration of theorem proving and model checking for system verification",
abstract = "Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find {"}bugs {"} in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.",
author = "Weiqiang Kong and Kazuhiro Ogata and Takahiro Seino and Kokichi Futatsugi",
year = "2005",
month = "12",
day = "1",
doi = "10.1109/APSEC.2005.9",
language = "English",
isbn = "0769524656",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
pages = "59--66",
booktitle = "Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05",

}

TY - GEN

T1 - A lightweight integration of theorem proving and model checking for system verification

AU - Kong, Weiqiang

AU - Ogata, Kazuhiro

AU - Seino, Takahiro

AU - Futatsugi, Kokichi

PY - 2005/12/1

Y1 - 2005/12/1

N2 - Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs " in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.

AB - Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs " in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.

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

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

U2 - 10.1109/APSEC.2005.9

DO - 10.1109/APSEC.2005.9

M3 - Conference contribution

AN - SCOPUS:33750242216

SN - 0769524656

SN - 9780769524658

T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC

SP - 59

EP - 66

BT - Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05

ER -