Newer
Older
---
layout: post
author: Pascal Cuoq
date: 2011-12-23 21:16 +0200
categories:
format: xhtml
title: "Z3 theorem prover in Microsoft Store, and retrocomputing Frama-C package"
summary:
---
{% raw %}
<p>This <a href="http://www.microsoftstore.com/store/msstore/en_US/pd/productID.242666500">page</a> where Microsoft Research's Z3 theorem prover is on sale for for just a bit less than $15 000 has come to my attention. This is interesting because Z3 is at the same time a <a href="http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/">free download</a>. Note that the free download is covered by <a href="http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/Z%203%20MSR-LA%20(2007-07-07).txt">this license</a> (executive summary: "non-commercial use only"). Presumably the $15 000 price tag buys you a more traditional license agreement.</p>
<p>I have two theories: the first is that the page is a mistake or a draft that was put online prematurely. The other is that Z3 is indeed now for sale for productive use which would be great news.</p>
<p>Z3 is an SMT solver that can be used among other applications as the last step of a program's verification through Hoare logic techniques. If you are from my generation and depending where you studied you may hazily remember from your studies applying Hoare logic rules by hand on simple programs... on paper. Well a decade's worth of research later it turns out it is much less tedious when the computer applies the rules automatically and then it even scales to moderately large functions whose verification may genuinely preoccupy someone.
For some examples Yannick Moy wrote a rather nice <a href="http://frama-c.com/jessie/jessie-tutorial.pdf">tutorial</a> introducing Jessie. Jessie is not the only tool that applies Hoare rules mechanically to verify a program against a specification. There's another one right in Frama-C named Wp in addition to all such verifiers that aren't Frama-C plug-ins.</p>
<p>Both Jessie and Wp can use Z3 in the last step of their work in which verifying a program against its specification is reduced to checking the validity of a number of logic formulas (you may have done that by hand during your computer science studies too and again it's much more fun when the computer does it).</p>
<p>I would be remiss if I didn't mention that for the same price as the "non-commercial use only" Z3 license you can get a commercial-use-allowing license for competing (and competitive) SMT prover <a href="http://ergo.lri.fr/">Alt-Ergo</a>. I expect that by contrast the $15 000 Z3 license includes bare-bones support but if that sum of money is burning a hole in your pocket you might also discuss the possibility of an agreement with the makers of Alt-Ergo. They are researchers with lots of competing demands on their time but you may be able to work something out.</p>
<p>Lastly if you are interested in Alt-Ergo and/or the Wp Frama-C plug-in and have a PowerPC Mac you're in luck! The last version (0.94) of Alt-Ergo is included in this semi-official <a href="http://www.mediafire.com/?vfmb6hsw08eeno0">retrocomputing Frama-C Nitrogen binary package</a> for Mac OS X Leopard PowerPC. <a href="/assets/img/blog/imported-posts/README_ppc">Click here</a> for the "readme" of that package. The package is mostly a celebration of the <a href="/index.php?post/2011/10/17/Features-in-Nitrogen-1">performance improvements in the value analysis in Nitrogen</a> that make it very usable on a G4 powerbook.</p>
{% endraw %}