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?