Keyword : symbolic model checking


Verifying Fault Tolerance of Concurrent Systems by Model Checking
Tomoyuki YOKOGAWA Tatsuhiro TSUCHIYA Tohru KIKUNO 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2002/11/01
Vol. E85-A  No. 11 ; pp. 2414-2425
Type of Manuscript:  Special Section PAPER (Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
Category: 
Keyword: 
symbolic model checkingfault toleranceSMVconcurrent systemguarded command
 Summary | Full Text:PDF(506.7KB)

Symbolic Model Checking of Deadlock Free Property of Task Control Architecture
Hiromi HIRAISHI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2002/10/01
Vol. E85-D  No. 10 ; pp. 1579-1586
Type of Manuscript:  Special Section PAPER (Special Issue on Test and Verification of VLSI)
Category: Verification
Keyword: 
verificationsymbolic model checkingdeadlockrobot control programconcurrent process
 Summary | Full Text:PDF(264KB)

Efficient Forward Model Checking Algorithm for ω-Regular Properties
Hiroaki IWASHITA Tsuneo NAKATA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1999/11/25
Vol. E82-A  No. 11 ; pp. 2448-2454
Type of Manuscript:  Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: 
Keyword: 
forward model checkingω-regular expressionlanguage emptiness checksymbolic model checkingformal verification
 Summary | Full Text:PDF(515.4KB)

A Partially Explicit Method for Efficient Symbolic Checking of Language Containment
Kiyoharu HAMAGUCHI Michiyo ICHIHARA Toshinobu KASHIWABARA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1999/11/25
Vol. E82-A  No. 11 ; pp. 2455-2464
Type of Manuscript:  Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: 
Keyword: 
formal verificationlanguage containmentsymbolic model checkingbinary decision diagram (BDD)ω finite automaton
 Summary | Full Text:PDF(748.1KB)

Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach--
Hiromi HIRAISHI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 1995/07/25
Vol. E78-D  No. 7 ; pp. 791-795
Type of Manuscript:  Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems)
Category: 
Keyword: 
formal verificationtime-space modal logicsymbolic model checkinglogic design verificationverification of bit-slice circuits
 Summary | Full Text:PDF(390.5KB)