F# release

Check out the community technology preview (i.e. pre-release of the "productized" version) of F#.

British pastimes...

cheers!

vacation.....actionscript

I'm on vacation/holiday......during my time off I've learned actionscript/flash programming. Aubrey and I wrote a game. See the result.

Paper on non-blocking algorithms

See our new paper: Proving that non-blocking algorithms don't block.

Balance.....

"It has long been my personal view that the separation of practical and theoretical work is artificial and injurious. Much of the practical work done in computing, both in software and in hardware design, is unsound and clumsy because the people who do it have not any clear understanding of the fundamental design principles of their work. Most of the abstract mathematical and theoretical work is sterile because it has no point of contact with real computing. One of the central aims of the Programming Research Group as a teaching and research group has been to set up an atmosphere in which this separation cannot happen. "

- Christopher Strachey

Finishing.......starting...........change..........

Congrats to my family: Aubrey graduated from primary school, Mina graduated from childhood; Bee is soon to be the shortest member of the family. ;-) Now we begin new adventures......

FMSB, WG2.3, Andrey, etc...

Why travel to conferences when all of the interesting people and meetings come to me? This summer's examples include Formal Methods in Systems Biology, WG2.3, Workshop on the Verification of Concurrent Algorithms, and visits by Andrey, Mooly and others.......

Rebooting "Communications of the ACM"

I was impressed by Moshe's article on upcoming changes to the CACM.

Imperial lectures, details.......

I will be giving 6 hours of lectures on `Proving termination and liveness of programs' at Imperial, in London. The times are 2-4 on Tuesday 27th May, Wednesday 28th May and Thursday 29th May in Room 145.

Good luck to Jim Larus!

Jim Larus dropped by our lab this week and gave us the rundown on Dan Reed's "Data Center Futures" group that he has joined.......

Automated reasoning group

On tuesday I'm giving another talk at the Automated Reasoning
Group's lunch talk series....

Off to Oxford, then MPI

I'm giving dept lectures at Oxford and MPI-SWS in the next few weeks....

Concurrency.....

I'm excited about this workshop that Mooly and Viktor are organizing at my lab........

A long time coming.....

Sometimes I find solutions to research questions to be very easy to find (e.g., we concieved and wrote up the paper "Proving thread termination" in perhaps 24 hours). This however was not the case for my new CAV paper "Proving conditional termination". You may find it simple now, but for some reason it took us years to develop this idea.

The research on this topic began as a conversation in 2006 between Mooly and I (in Tom Ball's office) after the first talk I gave at MSR-Redmond on Terminator. As visitors
to my lab came and went (e.g. Mooly, Sumit, Andrey, Tal) the thing snowballed into an ever growing ruckus carried out over visits and conference calls......co-authors would disagree and go off and write their own drafts, argue, plead, make alliances against each other, etc. It was terrifically fun, but I began to wonder if we'd ever find a workable solution. Finally, this winter, we got some traction and developed essentially what is in the paper today. After many many drafts, many failed starts, etc, the final version of the paper is finally done. Sigh.

Mooly is coming back to my lab this week.......I wonder what troublesome research question he'll propose this time ;-)

Proving conditional termination

Here are the slides from a talk on proving conditional termination that I gave at CMU.