DocumentCode
1953057
Title
Towards software model checking using MDGs
Author
Krykhtin, M. ; Mokhtari, Y. ; Mohamed, O. Ait ; Song, X.
Author_Institution
ECE Dept., Concordia Univ., Montreal, Que., Canada
fYear
2004
fDate
20-23 June 2004
Firstpage
345
Lastpage
348
Abstract
In this paper, we discuss the integration of multiway decision diagrams (MDG) model-checker into Bandera framework. A schema is introduced for transforming the Bandera intermediate representation (BIR) into the language of MDG model checker. Experience with model checking the Java programs demonstrates that this approach offers effective support for verifying software models.
Keywords
Java; decision diagrams; program verification; Bandera intermediate representation; Java program; model checker; multiway decision diagrams; software model checking; Concurrent computing; Debugging; Hardware; Humans; Java; Logic; Object oriented modeling; Power system modeling; Software tools; Yarn;
fLanguage
English
Publisher
ieee
Conference_Titel
Circuits and Systems, 2004. NEWCAS 2004. The 2nd Annual IEEE Northeast Workshop on
Print_ISBN
0-7803-8322-2
Type
conf
DOI
10.1109/NEWCAS.2004.1359103
Filename
1359103
Link To Document