GMC
The Monte Carlo Software Model Checker
| | | | |
 Introduction

During the past 15 years, GCC has evolved from a modest C compiler, to a full-blown, multi-language compiler that can generate code for more than 30 architectures. During the past year, the Tree-SSA branch of GCC has merged with the main line, resulting in the addition of two new intermediate languages: GENERIC, which provides a common infrastructure for abstract syntax tree analysis and optimization; and GIMPLE three-address code, which provides a common infrastructure for CFG (control ow graph) analysis and optimization. Together with their associated APIs, GENERIC and GIMPLE make Tree-SSA suitable as a platform not only for the development of high-level code optimization techniques, but also for new static analysis tools, applicable to all of GCC's input languages.

Using Tree-SSA, we have developed a suite of static analysis tools for GCC, including a CFG-based interpreter, slicer, a BDD-based model checker, and a Monte Carlo model checker. 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 uchi automata to realize a one-sided error, randomized algorithm for LTL model checking. Our experimental results demonstrate that this approach yields a highly efficient and scalable software model checker for GCC.

We implemented a software model checker for C based on the generic Monte-Carlo model-checking algorithm. Our model checker, GMC, is GCC based: it takes as input a C program, the target program to be verified, and a C function, the property function representing the LTL property of interest. The target program can contain concurrency primitives like in verisoft. In the case of safety properties, the property function is called to check for property violations in the target program. In the case of liveness properties, the property function is called to check if an accepting state of the target program is visited in nitely often, viewing the target program as a succinct representation of a Buchi automaton.

 

Maintained by Xiaowan Huang