Towards software model checking using MDGs
M. Krykhtin, Yassine Mokhtari, Otmane Aı̈t Mohamed, Xiaoyu Song · The 2nd Annual IEEE Northeast Workshop on Circuits and Systems, 2004. NEWCAS 2004. · 2004
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.