Grinder is a prototype tool for verifying C programs using graph-representation of computations.
The idea is to rearrange programs such that given a bound k, each computation can be explored according to any tree decomposition of width k of the corresponding behaviour graph. This produces under-approximations parameterized on k, which result in a complete method when we restrict to classes of behaviour graphs of bounded tree-width.Given a C program, Grinder converts it into another C program, working as a pre-processor for many state-of-the-art verification back-ends.
Grinder supports the following tools:
For instructions on how to install and run Grinder, please refer to one of the download packages above. The most recent is recommended.
The initial experiments are proof-of-concepts, meant to show that the theory behind Grinder may indeed lead to practical implementations that work in practice.
We considered a set of toy examples, simple test cases, each in both the safe and the unsafe variants.
We preprocessed them with Grinder and then verified them using CBMC.
For all the test case considered, the output from Grinder was verified to be equivalent to its corresponding original file (i.e., Grinder's output is SAFE if and only if the original file is SAFE).
Command-line to run Grinder on the original file:
./grinder.py -i simple_safe.c -t4 > simple_safe.test.cCommand-line tu run CBMC on the output file from Grinder:
cbmc --unwind 9 simple_unsafe.test.c > simple_unsafe.test.c.log
For further detail about the experiments, please refer to the publication below as well as the Grinder-0.1 package above available for download, which along with a README.txt file with instructions on how to install and run Grinder, includes everything necessary to replicate the experiments. In particular, for each test case the archive contains: (1) the original input file, (2) the output from Grinder, (3) the log of the verification with CBMC.