Irad Yavneh: Megilat Hamuamad 2005

A recent visit to Israel exposed me to this brilliant piece (in Hebrew). There are a few subsequent performances by Irad that are equally good. You can find them all at http://www.youtube.com/user/shaulm

SAFE Tech Fair Posters

QVM Tech Fair Poster

(click to see full size image)

Vista Pains

I really wanted to like Vista. When I got my Thinkpad X61 Tablet, it came with Vista installed by default. Ignoring the negative Vista press and applying wild optimism, I was sure that this is the beginning of a wonderful friendship. Unfortunately, this was not meant to be. Not only that Vista crashes left and right, it is always somebody else's fault: "Problem is caused by Intel Graphics Driver", "Problem is caused by Cygwin", and my all time favorite "This problem is being researched".


The utility may be called "Solve problems on your computer", but in the several months I had Vista, it did not help me find a solution to a single problem. All it really does is allocate blame, elsewhere.

To see how bad things are, here's a report from the performance and reliability monitor.

As you can see by the red markers, almost no day goes by without some sort of a failure. In some days, there are multiple failures. I already started booting to my Ubuntu on most days, but even for my sparse use of windows, I will probably roll back to XP soon.

Carl Sagan on the Importance of Scientific Research, May '93

Mark Wegman gave an interesting talk on the upcoming grand challenges in CS. In his talk, he used a snippet from this Carl Sagan clip. I thought that the message in this clip is worth echoing by posting it here.

The Right Stuff

On a Saturday afternoon, Greta, Martin and me enjoyed this ale (mostly its name, actually). The meat that accompanied it was cooked in a range from running-rare to nuclear-well-done... the chef was mostly hitting the end points of this range.

Workshop on the Verification of Concurrent Algorithms

Four of the nomads attended the Cambridge workshop on the verification of concurrent algorithms. I gave an overview talk on Shape Analysis for concurrent programs (slides). Martin gave a short talk about our work on synthesis of concurrent set algorithms (slides).

On the last day, we had a few hours before our flight, so we went punting. Below are a couple of pictures taken by Noam (you can see Noam's reflection in my sunglasses).

Now this is quality paper reviewing

Without a doubt, the most helpful and well thought out paper review I have ever received. This is the review in its entirety, except for the two-sentence summary of the paper which is excluded.

"The proposed technique appears to be novel. The authors have implemented the technique and evaluated on several significant software systems. The results are very promising."

QVM Talk

Just gave a QVM talk in Dagstuhl seminar on Scalable Program Analysis.
The slides are available here: http://kathrin.dagstuhl.de/08161/Materials2/

QVM: From 16.5K to 10K in 1 hour

This is a story that should serve as a warning to all people submitting to conferences. The tragic part is mostly the fact that we have learned that lesson
so many times, and still manage to ignore it... here goes...

When we wrote our QVM submission for OOPSLA, we assumed that the rules of the game are: ACM SIGPLAN template, 20 page limit. These are pretty reasonable rules. To be honest, we were quite pleased with our ability to describe things nicely and in sufficient detail using this format.

A few hours before the deadline (no more than 2), we decided to verify that our
nice submission indeed conforms to the OOPSLA submission directions. Much to our surprise, a strict 10,000 words limit accompanied the 20 page limit. A quick word-count of our submission yielded the fantastic number of 16,500 words... a mere 65% over the limit.

What followed can be only described as a major slash-and-burn frenzy in which whole sections of the paper went out. After a lot of work we reached the more reasonable limit of 12,000 words. Needless to say, the aforementioned "nice and in detail" was no longer a valid description of the paper. However, we believe that we maintained some of the essence of the paper in a reasonable form. (A final word count, without tables and figures, produced a number that was sufficiently close to 10,000 words.)

Some of the things that were described in the slashed 4000 words are:
- formal descriptions of certain components, notably the typestate histories
- some implementation details of typestate history and debug information
- implementation details of parallel checking of heap assertions
- additional experimental evaluation of the heap assertions
- also lost were various discussions of future extensions and optimizations
- references to our online supplement material (see below).

Here are some of the experiment logs recording (some of) our experience with QVM over various benchmarks:

Azureus (here are some bug reports bug1,bug2,bug3,bug4,bug5)
EclipseTrader
GOIM
Feed'NRead

coming soon