Author List
Japanese Page
SITE TOP
Login
To browse Full-Text PDF.
>
Forgotten your password?
Menu
Search
Full-Text Search
Search(JPN)
Latest Issue
A Fundamentals
Trans.Fundamentals.
JPN Edition(in Japanese)
B Communications
Trans.Commun.
JPN Edition(in Japanese)
C Electronics
Trans.Electron.
JPN Edition(in Japanese)
D Information & Systems
Trans.Inf.&Syst.
JPN Edition(in Japanese)
Abstracts of JPN Edition
Trans.Fundamentals.
Trans.Commun.
Trans.Electron.
Trans.Inf.&Syst.
-
Archive
Volume List
Trans.Fundamentals.
Trans.Commun.
Trans.Electron.
Trans.Inf.&Syst.
Transactions (1976-1990)
Volume List [JPN Edition]
A JPN Edition(in Japanese)
B JPN Edition(in Japanese)
C JPN Edition(in Japanese)
D JPN Edition(in Japanese)
-
Editorial Board
Editorial Board
Trans.Fundamentals.
Trans.Commun.
Trans.Electron.
Trans.Inf.&Syst.
Archive
Editorial Board[JPN Edition]
A JPN Edition(in Japanese)
B JPN Edition(in Japanese)
C JPN Edition(in Japanese)
D JPN Edition(in Japanese)
Archive
-
Open Access Papers
Trans. Commun. (Free)
Trans. Commun.
Trans. Commun.(JPN Edition)
Trans. Electron. (Free)
Trans. Electron.
Trans. Electron.(JPN Edition)
Trans. Inf.&Syst. (Free)
Trans. Inf.&Syst.
Trans. Inf.&Syst.(JPN Edition)
-
Link
Subscription
For Authors
Statistics:
Accepting ratio,review period etc.
IEICE Home Page
-
Others
Citation Index
Privacy Policy
Copyright & Permissions
Copyright (c) by IEICE
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
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
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