Skip to content

CBMC starter kit running proofs

Jump to bottom
Mark R. Tuttle edited this page Oct 28, 2020 · 1 revision

You can run an individual proofs or all proofs concurrently.

Running a single proof

To run a single proof, go to the directory containing the proof and type make report. This will build the goto binary for CBMC, run CBMC, and run CBMC viewer to produce a summary of the results. A standard sequence of commands is

cd FUNCTION
make report
open html/index.html

Running all proofs

To run all proofs, go to the proof root and run the script run-cbmc-proofs.py.

Clone this wiki locally