Grosu/Huang/Jain/Smolka: Open Source Model Checking
## Open Source Model Checking*

*Radu Grosu, Xiaowan Huang, Sumit Jain and Scott A. Smolka*
We present GMC2, a software model checker for GCC, the open-source
compiler from the Free Software Foundation (FSF). GMC2, which is part
of the GMC static-analysis and model-checking tool suite for GCC under
development at SUNY Stony Brook, can be seen as an extension of
*Monte Carlo model checking* to the setting of concurrent,
procedural programming languages. Monte Carlo model checking is a
newly developed technique that utilizes the theory of geometric random
variables, statistical hypothesis testing, and random sampling of
lassos in Buechi automata to realize a one-sided error, randomized
algorithm for LTL model checking. To handle the function call/return
mechanisms inherent in procedural languages such as C/C++, the version
of Monte Carlo model checking implemented in GMC2 is optimized for
pushdown-automaton models. Our experimental results demonstrate that
this approach yields an efficient and scalable software model checker
for GCC.

*In Proceedings of SoftMC'05, the 3rd Workshop on Software Model Checking,
July 2005, Edinburgh, UK.10*

*R. Grosu, X. Huang and S. Jain were partially supported by the NSF
Faculty Early Career Development Award CCR01-33583.