An Old Tutorial for Running Boogie and Z3 on Linux (for .NET 2.0)
Software verification tools that I have built in the last couple of years use the combination of Boogie verification condition generator and Z3 SMT solver as their back end. Both Boogie and Z3 are developed by Microsoft Research, and therefore, understandably, Windows is their platform of choice. However, I’ve often had a need to use Boogie and Z3 on Linux, since some of my tools (e.g. SMACK) are Linux based. Next, I am going to describe how I managed to pull that off (disclaimer: there are probably better ways of doing this, but this one worked for me and that’s good enough)…
I am using openSuse 11.2 (Linux version 188.8.131.52), although I am sure this would work on other Linux distributions/versions as well. Before we start, you will, of course, also need Boogie and Z3 binaries, which you can get from the respective websites. Make sure you copy z3.exe into Boogie’s bin folder and run Boogie under Windows to see if it works.
Let’s go into Linux now. To be able to run z3.exe, install wine (I am using wine-1.1.28) and download the winetricks script (I am using winetricks version 20090815). Then, using winetricks install vcrun2008
Now try typing
wine z3.exe /h
to see if Z3 is working.
For Boogie you will have to install support for .NET (i.e. dotnet20), again using winetricks
See if Boogie is working by typing
Note that I do get some weird error messages (e.g. fixme:shell:URL_ParseUrl failed to parse L”Core”), but those (surprisingly) don’t seem to matter, everything still works.
Finally, check if Boogie/Z3 combination is working together and execute
wine Boogie.exe some_simple_bpl_file.bpl
And voila, you are done!
Note that I tried many other combinations as well (e.g. mono + wine), but this one seems to work the best. Any feedback would be appreciated, especially if you figure out how to get rid of those annoying error messages .
You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.