Zvonimir Rakamaric

A Tutorial for Running Boogie and Z3 on Linux

2010-12-03T16:35:00.000-08:00

I just learned that Boogie recently switched to using .NET 4, and therefore the tutorial on how to run Boogie under Linux using .NET 2 I wrote a couple of months ago is now deprecated. I played a little bit with the latest version of Boogie under Linux and managed to get it to work, this time using Mono.

So, first you have to get a Linux binary of Z3. You can always download the latest SMT Competition Z3 Linux binary from the Z3's download page (look for Other platforms). Copy the bin/z3 executable into Boogie's folder and rename it to z3.exe.

Alternatively, you can try to get the Windows Z3 binary to work under Linux using wine. So, 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

winetricks vcrun2008

Now try typing

wine z3.exe /h

to see if Z3 is working. For Boogie to be able to call Z3, you still have to achieve that z3.exe can be executed without the wine command in front. This is the tricky part that is accomplished using binfmt_misc and doing the following:

su
mount binfmt_misc -t binfmt_misc /proc/sys/fs/binfmt_misc
echo ':DOSWin:M::MZ::/usr/bin/wine:' > /proc/sys/fs/binfmt_misc/register

Try calling Z3 without wine

z3.exe /h

to see if Z3 is still working.

Second, install the latest version of Mono that supports .NET 4. Boogie is going to fail if the environment variable ProgramFiles is not set, but you can fool it by setting ProgramFiles to essentially anything:

export ProgramFiles=/home/

Create a simple bpl file test.bpl and check if just Boogie without Z3 is working using Mono:

mono --runtime=v4.0.30319 Boogie.exe test.bpl /noVerify

Finally, check if Boogie/Z3 combination is working together and execute:

mono --runtime=v4.0.30319 Boogie.exe test.bpl

You can also get rid of the ugly --runtime switch, if you edit Boogie.exe.config like this:

<?xml version="1.0"?>
<configuration>
   <startup>
     <supportedRuntime version="v4.0.30319" sku=".NETFramework,Version=v4.0"/>
   </startup>
</configuration>

And voila, you are done!
I would like to thank Vladimir Klebanov for his valuable feedback and help, and any additional feedback, comments, or improvements would be appreciated.

Updated Guidebook for Graduate Studies Abroad

2010-12-03T09:03:00.000-08:00

Domagoj and I recently added some new material to our Guidebook for Graduate Studies Abroad and this 2nd extended online edition is now available for download.

Uploaded the camera-ready version of the POPL 2011 delay-bounded scheduling paper

2010-11-12T10:21:00.000-08:00

Word cloud summary of the POPL 2011 paper.

The final, camera-ready version of the delay-bounded scheduling paper is now available and can be obtained here. Inspired by others, I also started playing with word clouds a little bit, and on the right you can find a nice word cloud summary of this paper. Enjoy!

Delay-bounded scheduling paper accepted to POPL 2011!

2010-10-04T18:03:00.000-07:00

The paper titled "Delay-Bounded Scheduling" I coauthored with Michael Emmi and Shaz Qadeer got accepted to the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011). The camera-ready version will be ready and available in a couple of weeks. In the meantime, those of you who are eager to learn what delay-bounded scheduling is all about can check out our tech-report.

An Old Tutorial for Running Boogie and Z3 on Linux (for .NET 2.0)

2010-06-30T10:55:00.000-07:00

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 2.6.31.12), 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

winetricks 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

winetricks dotnet20

See if Boogie is working by typing

wine Boogie.exe

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 .

Paper on context-bounded analysis accepted at SPIN 2010

2010-06-25T09:37:00.000-07:00

The work I did with Naghmeh and Alan on empirical evaluation of context-bounded translations for concurrent software was accepted at SPIN 2010. We investigate source-to-source translations: a concurrent program, given a bound on the number of context switches, is translated into a corresponding sequential program. In the paper, we compare three different translations in the verification-condition-checking (using SMT solvers) paradigm. We evaluate their scalability under a wide range of experimental conditions: we draw interesting conclusions and provide practical guidance for using context-bounded analysis in a VC-checking paradigm.

The final version of this paper is available here.

And here is what Shaz Qadeer said about the paper: "I really like the paper, quite independent of its focus on evaluation of context-bounded translations. There are very nice insights in the paper about the difference between finite-state symbolic model checking and the VC-based techniques. In fact, I would recommend this paper to anybody who has a model checking background and is beginning to use theorem provers." Thanks a lot Shaz!

Joining Cadence Research Laboratories

2010-06-19T10:39:00.000-07:00

I am excited to announce that I'll be joining Cadence Research Laboratories in fall! I am going to continue doing research on effective, automatic techniques for analysis, verification, and testing of software. Most likely I'll be moving to the Bay Area in October.

Won silver medal in the ACM Student Research Competition at ICSE 2010!

2010-05-17T13:43:00.000-07:00

Woohoo! I won silver medal in the ACM Student Research Competition at ICSE 2010 with my competition entry titled "STORM: Static Unit Checking of Concurrent Programs". It was a tough competition, with Code Bubbles winning gold and Thomas Fritz, also from UBC, taking bronze. Furthermore, this is not the end of the story for STORM since top three winners are invited to compete in the ACM Student Research Competition Grand Finals.

Static analysis in real world

2010-02-17T14:28:00.000-08:00

Communications of the ACM (CACM) recently published an article titled "A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World". Written by the Coverity crowd, the article talks about their experience with commercializing a static bug-finding tool. The authors list practical problems they run into that you typically wouldn't see when building a research prototype, and also describe how they solved (or worked around) them. Interesting and entertaining...

Participating in the ACM Student Research Competition at ICSE 2010

2010-02-16T23:12:00.000-08:00

My short paper about STORM, a concurrency checker I've been working on in the past year or so, got accepted into the second round of the ACM Student Research Competition at ICSE 2010. I'll be going to Cape Town soon to try to win one of the main prizes. Sweet!

Started another internship at Microsoft Research

2009-11-26T11:13:00.000-08:00

This is my third internship at Microsoft Research, it seems I just can't get enough of that place :).
I'll be working again with Shaz Qadeer and Shuvendu Lahiri in the RiSE team. The main goal of the internship is to find important concurrency bugs in Microsoft's software using my concurrency checker called STORM. Exciting!

Amir Pnueli dies at 68

2009-11-15T17:21:00.000-08:00

The New York Times published an article about the recently deceased pioneer of formal verification Dr. Amir Pnueli:
Amir Pnueli, Pioneer of Temporal Logic, Dies at 68

Passed my PhD thesis proposal defense

2009-11-10T17:27:00.000-08:00

Today I passed my PhD thesis proposal defense and finally squared that off! I believe I am now a PhD candidate :). I got very useful feedback from my committee members that is definitely going to make my thesis stronger. So a big thanks for that to Alan, Ken, and Mark. Thanks to Eric as well for chairing the defense.

Visited IST Austria

2009-10-23T01:14:00.000-07:00

A couple of days ago, I visited the Institute of Science and Technology (IST) Austria in Klosterneuburg near Vienna. IST Austria is a brand new research institution on track to become a world-class research center. I was invited by its president Prof. Tom Henzinger to give a talk about my research on verification of concurrent systems code. I was impressed by smooth organization of my visit, people who work there and their research, as well as institute's surroundings in the Vienna Woods.
Thanks again to everybody at the IST Austria who made my stay a very pleasant one!

Attending Dagstuhl Seminar

2009-10-08T04:37:00.000-07:00

I am attending Dagstuhl Seminar titled "Interaction versus Automation: The two Faces of Deduction". I gave a talk there about my work on the verification of concurrent systems code using SMT solvers.

Visited Intel Strategic CAD Labs in Hillsboro

2009-08-08T14:52:00.000-07:00

I was invited recently to visit John O'Leary's group at Intel Strategic CAD Labs in Hillsboro, OR, USA. So, last week I visited them for a day. I gave a talk about my work on verification of concurrent systems code. Also, I had interesting in-depth conversations with John, Amit, and Jim about my tool SMACK and my concurrency related research, as well as their software verification work. I am glad there are a few more guys out there working on software verification and checking. They are very interested in using SMACK or parts of it in their own projects, so I am excited about this possible future collaboration.

Visited Verimag in Grenoble

2009-06-25T19:14:00.000-07:00

I gave an invited talk about my recent work on finding concurrency errors in systems code at Verimag in Grenoble, France. Verimag is a very nice place and it was a pleasant visit. I would like to thank Radu Iosif again for hosting me.

Final version of my CAV 2009 paper is out

2009-04-23T12:56:00.001-07:00

I posted the final version of my CAV 2009 paper "Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers" on my homepage. Check it out!
And comments and/or questions are always appreciated.

Paper accepted to CAV 2009!

2009-03-27T09:21:00.000-07:00

The paper on static context-bounded analysis of systems software I coauthored with Shuvendu and Shaz got accepted to 21st International Conference on Computer Aided Verification (CAV 2009). I am really excited about this work and glad it got in. I'll put the final version of the paper on my homepage soon, so be sure to stop by again and check it out. And off to France in June!

STTT paper published - my first journal publication

2009-02-23T17:47:00.000-08:00

Almost two years ago, me and my coauthors got invited to submit the extended version of our TACAS 2007 paper to a special issue of the International Journal on Software Tools for Technology Transfer (STTT). Last weekend I received an email that our journal paper titled "A Low-Level Memory Model and an Accompanying Reachability Predicate" got published. Finally :)!

Received Dagstuhl Seminar invitation

2009-02-16T14:31:00.000-08:00

Awesome news! I got invited to the Dagstuhl Seminar "Interaction versus Automation: The Two Faces of Deduction"! Dagstuhl seminars are invitation-only computer science seminars held in Germany. They bring together established scientists as well as promising young researchers, with the goal to promote open, in-depth discussions and collaboration on the topic of interest.
I am looking forward to visit Germany in October. I am sure it'll be a great and productive experience.

Gave a talk at VMCAI 2009 on a scalable memory model for low-level code

2009-01-23T09:30:00.001-08:00

It was the last talk of the last session of the last day of the conference, but quite a lot of people still decided to stick around (I hope because they were interested in the paper I presented :)), which was awesome. I think the presentation went well. As always, I also enjoyed VMCAI in general. Now I am attending POPL and in parallel working on my CAV paper. Busy week....

With Storm, I wrapped up another awesome internship at MSR Redmond

2009-01-17T15:32:00.000-08:00

I finished my internship at the RiSE group at Microsoft Research in Redmond last week. It was again an awesome experience. The initial idea for the internship project was: "Hmm, let's statically find concurrency related bugs in device drivers.". Easier said then done :).
But after many days of hard work, we (meaning me and my MSR mentors Shuvendu and Shaz, who are, btw, great guys!) had a working prototype of a tool for finding concurrency related bugs in systems code. Tool's codename is Storm, inspired by unusual weather conditions in Redmond in December :) (the photo shows the view from my office on one Sunday afternoon).

We applied Storm on a number of real Windows device drivers and found a concurrency related bug that couldn't be discovered using any of the other static analysis tools they have. Furthermore, the bug was confirmed and fixed by developers, which got them very interested in the project. There is still a lot of work to be done, and I believe Storm is going to stick around for a while. Pretty good for only three months of work, and on top of that, there is still a paper to be written.... What can I say, maybe I should do another internship there before I graduate :)...

Linux buffer-overflow bugs got Smack-ed

2008-12-26T15:30:00.000-08:00

Using my static analysis tool called Smack, I found a couple of buffer-overflow bugs in the Linux kernel device drivers a few moths ago. Two of them (Bug #11399 and Bug #11408) got fixed in the last release (2.6.28). This is a great incentive to try to find some more.

CRA Taulbee Survey - an interesting survey for CS graduate students

2008-12-12T10:41:00.000-08:00

The Computing Research Association (CRA) publishes the Taulbee Survey every year. The survey provides information on the enrollment, production, and employment of Ph.D.s in computer science and computer engineering, and also on faculty salaries across North America.
The last survey (2006/07) predicts a peek of production of Ph.D.s in this and the following year, and then a small decline. We'll see...

Reorganized my homepage and started this blog (of sorts)

2008-12-07T19:08:00.000-08:00

Since I hurt my back playing basketball on Friday, I had to spend this weekend pretty much in bed (and miss the MSR Christmas party :(). With all that time on my hands and nothing to do (I can't work remotely for MSR), I invested a few hours in reorganizing my homepage. Nothing fancy, just moved things around a bit.
And I started this blog!

Visiting MSR in Redmond until mid January

2008-12-07T18:35:00.000-08:00

I am a research intern in the newly formed RiSE group at the Microsoft Research in Redmond. With my mentors Shuvendu Lahiri and Shaz Qadeer, I am looking into new ways for statically finding concurrency related bugs in device drivers. Very cool stuff!

Formal methods in The New York Times

2008-12-06T21:57:00.000-08:00

Formal methods got mentioned in a recent article published in the The New York Times on testing of the new Intel's chip code-named Nehalem.

I gave a short statement for the Croatian National Television about the MSR fellowship

2008-02-14T22:28:00.000-08:00

Domagoj Babic's and mine 2 minutes of fame in science news on the Croatian National Television (HRT 1). We talked about the Microsoft Research Fellowships we received. The entire interview can be seen on YouTube.

I received the 2008 Microsoft Research Fellowship

2008-01-31T22:36:00.000-08:00

Yes, finally I got it! I received the 2008 Microsoft Research Fellowship:
"Congratulations! We are pleased to announce your selection as a Microsoft Research Fellow. Competition for our Fellowships was extremely intense as we received over 140 very highly qualified applications. We conducted interviews with 56 applicants for 12 Microsoft Research fellowships and four Microsoft Live Labs fellowships. Thus, your selection for this award is a tremendous honor and recognition of your accomplishments."