SE547: BDDs: Software Model Checking [5/22]

Software model checkers translate source code into (possibly big!) logical formulas. For example:

  void foo (int x, int y) {
    char[] z = new char[x+1];
    if (y < x) { z[y] = 'a'; }
  }

Is this program safe? What logical formula do we generate from it?

We have turned the problem of software model checking into the problem of logical satisfaction.

More on software model checkers later...