StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>The short answer is: “no, nobody tried to prove Z3 using Z3 itself” :-)</p> <p>The sentence “we proved program X to be correct” is very misleading. The main problem is: what does it mean to be correct. In the case of Z3, one could say that Z3 is correct if, at least, it never returns “sat” for an unsatisfiable problem, and “unsat” for a satisfiable one. This definition may be improved by also including additional properties such as: Z3 should not crash; the function X in the Z3 API has property Y, etc.</p> <p>After we agree on what we are supposed to prove, we have to create models of the runtime, programming language semantics (C++ in the case of Z3), etc. Then, a tool (aka verifier) is used to convert the actual code into a set of formulas that we should check using a theorem prover such as Z3. We need the verifier because Z3 does not “understand” C++. The Verifying C Compiler (<a href="http://research.microsoft.com/en-us/projects/vcc/" rel="noreferrer">VCC</a>) is an example of this kind of tool. Note that, proving Z3 to be correct using this approach does not provide a definitive guarantee that Z3 is really correct since our models may be incorrect, the verifier may be incorrect, Z3 may be incorrect, etc.</p> <p>To use verifiers, such as VCC, we need to annotate the program with the properties we want to verify, loop invariants, etc. Some annotations are used to specify what code fragments are supposed to do. Other annotations are used to "help/guide" the theorem prover. In some cases, the amount of annotations is bigger than the program being verified. So, the process is not completely automatic. </p> <p>Another problem is cost, the process would be very expensive. It would be much more time consuming than implementing Z3. Z3 has 300k lines of code, some of this code is based on very subtle algorithms and implementation tricks. Another problem is maintenance, we are regularly adding new features and improving performance. These modifications would affect the proof.</p> <p>Although the cost may be very high, VCC has been used to verify nontrivial pieces of code such as the Microsoft Hyper-V hypervisor.</p> <p>In theory, any verifier for programming language X can be used to prove itself if it is also implemented in language X. The <a href="http://research.microsoft.com/en-us/projects/specsharp/" rel="noreferrer">Spec#</a> verifier is an example of such tool. Spec# is implemented in Spec#, and several parts of Spec# were verified using Spec#. Note that, Spec# uses Z3 and assumes it is correct. Of course, this is a big assumption.</p> <p>You can find more information about these issues and Z3 applications on the paper: <a href="http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf" rel="noreferrer">http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf</a></p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload