I successfully defended and wrapped up my PhD! Yaaaay!

Big thanks goes to my advisor Alan Hu, committee members Mark Greenstreet and Ken McMillan, university examiners Gail Murphy and Karthik Pattabiraman, as well as my external examiner Ranjit Jhala. The final version of my PhD thesis is available online and can be found here.

Soon after I wrapped up my PhD, I joined Carnegie Mellon University in Silicon Valley as a postdoctoral fellow. Here I am working on a NASA-funded project and collaborating with Dimitra Giannakopoulou and Vishwanath Raman. The goal of the project is improving coverage of testing and checking of NASA’s air traffic control system using compositional techniques. I am sure that lots of challenging and exciting work is ahead of me!

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.

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.

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!

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.