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
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;
Conference_Titel :
Circuits and Systems, 2004. NEWCAS 2004. The 2nd Annual IEEE Northeast Workshop on
Print_ISBN :
0-7803-8322-2
DOI :
10.1109/NEWCAS.2004.1359103
