Darko Poposki, Risto Petroski, Dimitar Stojkovski, Guido Sciavicco
University of Information Science and Technology - Ohrid, Macedonia
April 12, 2011
Formal verification of low-level software has become a trend in the formal methods community. Over the past decade, there has been considerable advancement in the theory and practice of automated formal software verification, and one of the most promising paradigms to emerge in this area is software model checking. In this work, we consider a possible application of this methodology to the verification of MIPS Assembly programs. We consider very small programs and very simple safety requirements, such as a register is never used before initialization. We present a newly developed, non-optimized, software system to this purpose, whose distinctive feature is being specifically tailored for MIPS programs, and that allows a number of possible generalization in the type and the scope of the properties that can be checked. This work has been undertaken while three out of four authors were first-year undergraduate students at the University of Information Science and Technology in Ohrid (Macedonia).
Please check document etai2011.pdf to find out more about this research.