[frik]

I heard Microsoft uses provers to check (automated verification) third party kernel mode device drivers. Is that the Z3 proofer? I searched on Google and got several results but the meaning of the term "kernel" is overloaded and means different things in operating systems and proofers/solvers.

[jonjacky]

This page says that the driver verifier uses the SLAM verification engine - I am not sure whether/how that is related to Z3:

http://research.microsoft.com/en-us/projects/slam/

[gsnedders]

SLAM2 uses Z3 for a few things, AIUI.

[ufo]

When people talk about kernels it has more to do with proof verification. Once you have written down a proof for something you need a way to verify is the proof is correct, checking for syntax errors, checking if each step is a valid inference step, etc. For the more advanced theorem provers what they tend to try to do is use a comlpex system to let the programmer build a proof thats easy to describe but in the end convert it to a longer proof that a simpler verifier can check.

As for Z3, its strength is about contraint solving. You can specify a set of constraints and it will try to find if there is a viable solution that satisfies the constraints. It includes a SAT (boolean satisfiability)solver and beefs it up with support for some higher level things, like integer arithmetic, bit vectors, etc. This kind of constraint solver is very useful for finding bugs: for example, the notorious intel floating point bug was found out by asking a SAT solver to find an input where the processor's circuit produced the wrong value.

[tedks]

This is the project webpage, though I can't recall if it uses Z3 or not: http://research.microsoft.com/en-us/projects/slam/

[frik]

Thanks. From that page:

  Pointers in SLAM2: Efficient evaluation of pointer 
  predicates with Z3 SMT Solver in SLAM2