LFX Videos now available

Videos from the recent LFX workshop are available here:
http://www.vimeo.com/groups/lfx

Slides are also available online on the workshop's homepage:
http://research.ihost.com/lfx2010/

Phalanx is to appear in ISMM 2010!

Our paper on Phalanx — a practical framework for dynamically checking expressive heap properties — was accepted to ISSM 2010. Phalanx uses novel parallel algorithms to efficiently check a wide range of heap properties including ownership, sharing and reachability.

Abstraction-Guided Synthesis to appear in POPL'10

Our paper titled "Abstraction-Guided Synthesis" will appear in POPL'10. The paper presents an approach for synthesizing synchronization in concurrent programs using abstract interpretation. Below is a word-cloud summary. The paper itself will be available online sometime early November.

Bell Labs

"Pierce created a rare environment in any industry or research lab, one in which the scientists felt empowered to do their best and in which creativity was highly valued. At the time, the Bell Telephone Company/AT&T had a complete monopoly on telephone service in the U.S. and a large cash reserve. Their laboratory was something of a playground for the very best and brightest inventors, engineers and scientists in America. In the Bell Labs 'sandbox', Pierce allowed his people to be creative without worrying about the bottom line or the applicability of their ideas to commerce. Pierce understood that the only way true innovation can occur is when people don't have to censor themselves and can let their ideas run free. Although only a small proportion of those ideas may be practical, and a smaller proportion still would become products, those that did would be innovative, unique, and potentially very profitable. Out of this environment came a number of innovations including lasers, digital computers, and the Unix operating system".

(from the book This is your brain on music / Daniel J. Levitin)

PSY 2009 videos now available online

On June, we held the 1st International Workshop on Practical Synthesis for Concurrent Systems (PSY 2009). In this workshop, we experimented with recording all the talks with a Vado HD (recommended by our gadget-guru Noam Rinetzky). The results are definitely far from a professional-level recording, but the cost of the entire setup was only a few hundred bucks.

The resulting videos are available here.

I think that the main lesson from these videos is to get a better tripod, preferably one with a bubble level.

The exact setup used for producing these videos:

Creative Vado HD 720p Camcorder with 8 GB and 2x Digital Zoom
Creative Labs Battery Charger for Vado and Vado HD Camcorders
Creative Labs Rechargeable Lithium Ion Battery for Vado HD Camcorder
Digipower TP-S010 flexible and sturdy ultra compact Mini Tripod
Handbrake video transcoder (thanks to Yoad for the reference)
Quicktime Pro for editing the videos (yes, you will have to edit the videos)
Vimeo Plus for hosting the videos

Total cost: ~$300 including 1yr of plus membership on Vimeo

QVM Word Clouds

Here's some more word cloud joy, now for the QVM OOPLSA'08 paper.



and for the QVM Chameleon PLDI'09 paper

Algorithms for Concurrent Data Structures

Word clouds seem to be all the rage lately. Playing with some clouds for a recent talk, I found them to actually provide an interesting summary of research papers. For example, here's a word cloud for our PLDI'08 paper on derivation of highly-concurrent linearizable data structure algorithms.

Apart from the emphasis of terms like "true", this is a pretty decent summary of what's going on in the paper --- concurrent algorithms, linearizability, and a lot of dance around atomic blocks, restarts, and the pointers curr and pred.