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 matrix,  bounded model checking,  invariant properties,  satisfiability modulo theories, 
  Summary |  Full Text:PDF (432.4KB)
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 framework,  formal methods,  the OTS/CafeOBJ method,  falsification,  verification, 
  Summary |  Full Text:PDF (533KB)
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 translation,  verification,  algebraic specification,  behavioral specification,  rewirte specification,  CafeOBJ,  Maude, 
  Summary |  Full Text:PDF (305.3KB)