Weiqiang KONG


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)

Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2010/05/01
Vol. E93-D  No. 5  pp. 974-984
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Specification
Keyword: 
e-Government messaging frameworkformal methodsthe OTS/CafeOBJ methodfalsificationverification
 Summary | Full Text:PDF(534.1KB)

A Specification Translation from Behavioral Specifications to Rewrite Specifications
Masaki NAKAMURA Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/05/01
Vol. E91-D  No. 5  pp. 1492-1503
Type of Manuscript:  PAPER
Category: Fundamentals of Software and Theory of Programs
Keyword: 
specification translationverificationalgebraic specificationbehavioral specificationrewirte specificationCafeOBJMaude
 Summary | Full Text:PDF(306.5KB)