Keyword : bounded model checking


Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras
Jefferson O. ANDRADE Yukiyoshi KAMEYAMA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/05/01
Vol. E95-D  No. 5 ; pp. 1355-1364
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
multi-valued model checkingbounded model checkingquasi-boolean logic
 Summary | Full Text:PDF(806.6KB)

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 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Vol. E94-D  No. 5 ; pp. 946-957
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
state transition matrixbounded model checkinginvariant propertiessatisfiability modulo theories
 Summary | Full Text:PDF(433.7KB)

Multi-Level Bounded Model Checking with Symbolic Counterexamples
Tasuku NISHIHARA Takeshi MATSUMOTO Masahiro FUJITA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2011/02/01
Vol. E94-A  No. 2 ; pp. 696-705
Type of Manuscript:  PAPER
Category: VLSI Design Technology and CAD
Keyword: 
formal verificationbounded model checkingfinite state machine with datapathsymbolic simulation
 Summary | Full Text:PDF(1.4MB)

Feature Interaction Detection by Bounded Model Checking
Tomoyuki YOKOGAWA Tatsuhiro TSUCHIYA Masahide NAKAMURA Tohru KIKUNO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2003/12/01
Vol. E86-D  No. 12 ; pp. 2579-2587
Type of Manuscript:  Special Section PAPER (Special Issue on Dependable Computing)
Category: Dependable Communication
Keyword: 
bounded model checkingSATfeature interaction
 Summary | Full Text:PDF(590.3KB)