Bug goto-cc – a C/C++ front-end for Verification

About goto-cc

goto-cc is a compiler that compiles programs given in a C and C++ into GOTO-programs (i.e., control-flow graphs). goto-cc can be run in the following environments:

The resulting goto-binaries are not meant to be executable, but are typically given to a verification or testing tool like SATABS or CBMC. As an additional feature, goto-cc generates dot-style flowgraphs of your functions!

You should also read the license.

goto-cc News

NEW: There is now a Google Group for annoucements related to the CPROVER tools.

NEW: goto-cc now processes most parts of the Linux Kernel without any need for modifications. The CPROVER manual contains instructions.


There is a section on goto-cc in the CPROVER manual.


You can get goto-cc (in binary and source form) by downloading and installing CBMC.



This research is currently supported by EPSRC grant EP/H017585/1.