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 - 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