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

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'A lightweight integration of theorem proving and model checking for system verification'. Together they form a unique fingerprint.

  • 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