The extensions mentioned above are typically less than a hundred lines of code. A practical result of our experience with MC is that the majority of our extensions were written by programmers who had only a passing familiarity with the systems that they checked. Although writing code that obeys system rules can be quite difficult, these rules are easy to express. Thus, writing checkers for many of them is relatively straightforward. This paper is laid out as follows.
Section discusses related work.
Section gives an overview of MC and the system we use to implement it. Section applies the approach to the C assert macro and shows that even in such a limited domain, MC provides non-trivial benefits. Section shows how to use MC to enforce ordering constraints such as checking that kernels verify user pointers before using them. Section extends this to global, system- wide constraints.