An SMT-based approach to bounded model checking of designs in state transition matrix

Weiqiang Kong, Tomohiro Shiraishi, Noriyuki Katahira, Masahiko Watanabe, Tetsuro Katayama, Akira Fukuda

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)


State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.

Original languageEnglish
Pages (from-to)946-957
Number of pages12
JournalIEICE Transactions on Information and Systems
Issue number5
Publication statusPublished - May 2011

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence


Dive into the research topics of 'An SMT-based approach to bounded model checking of designs in state transition matrix'. Together they form a unique fingerprint.

Cite this