SE547: CBMC: CBMC Algorithm [6/19]

How cbmc works:

1) Start with a C program with assert(...) and assume(...) statements.

2) Preprocess the program: just left with functions, loops, if, goto and assignment.

3) Unwind function calls, loops and goto: just left with if and assignment.

4) Rename all variables to be unique.

5) Calculate the constraints of the program C, and the properties we're checking of the program P.

6) Hand off checking C P to a SAT-solver.

Hooray, we've translated an undecidable problem into an NP-complete problem: where has all the work gone?