Recall...
What is a buffer overflow attack?
What is the result of a successful buffer overflow attack?
What can we do about buffer overflows?
What is a SAT-solver?
What is a software model checker?