Open-Source Model Checking

We present GMC2 , a software model checker for GCC, the opensource 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 B

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Smolka
• Keywords: Checking, ENTCS 2006, Monte Carlo Model, Software Model