5 ms·

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 se

by frik 12y ago

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.

tedks 12y ago
This is the project webpage, though I can't recall if it uses Z3 or not: http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/
- frik 12y ago
  Thanks. From that page: Pointers in SLAM2: Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2
ufo 12y ago
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.
jonjacky 12y ago
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/ http://research.microsoft.com/en-us/projects/slam/
- gsnedders 12y ago
  SLAM2 uses Z3 for a few things, AIUI.

by frik 12y ago

tedks 12y ago

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

frik 12y ago
Thanks. From that page: Pointers in SLAM2: Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2

ufo 12y ago

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.

jonjacky 12y ago

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/ http://research.microsoft.com/en-us/projects/slam/

gsnedders 12y ago
SLAM2 uses Z3 for a few things, AIUI.