SE547: CBMC: Software Model Checking [3/19]

Goal of a software model checker: to ensure a program is safe. What does this mean?

What are example safety properties we might expect for C programs?

Imagine we have a function boolean safe(String filename) which decides safety: how can we reach a contradiction?

This means that verifying safety is undecidable. What can we do about it?

Common solution to undecidability: bounded model checkers.