Congratulations to Eric Koskinen

Congratulations to my (now former) PhD student Eric Koskinen who successfully defended his PhD today!

Bio Model Analyzer (BMA)

We're announcing the first release of our tool for analyzing biological models.
Here's a pointer to the paper: Here's a pointer to the tool:

UCL

A number of us are leaving Queen Mary, University of London and moving to University College London. Yes, yes, I'm staying at Microsoft Research....my appointment at UCL joint with Microsoft Research.

New papers on liveness proving

Making prophecies with decision predicates shows how LTL can be lazily reduced to CTL with some help of automatically inferred "prophecy variables".

Temporal property verification as a program analysis problem shows how known tools can be used to prove CTL properties of infinite state programs

New papers

I've recently been working on approaches to automatically verify properties of biological models, as well as relooking at ways of proving temporal properties of programs. This research has resulted in some new papers:

Congrats to Andrey Rybalchenko!

Andrey Rybalchenko was listed as one of MIT's selective set of 2010 Young Innovators Under 35 (TR34). Way to go Andrey!

Congratulations to Alexey Gotsman

Alexey Gotsman completed his PhD this week. Well done Alexey!

Congrats to Viktor Vafeiadis

Viktor Vafeiadis has won this year's SIGPLAN Doctoral Dissertation Award. Well done!

A new look at hardware synthesis

Check out the draft of a paper we've written on hardware synthesis.

See also: PPT slides that Satnam and I presented to Bill Gates.

Berkeley lectures

I'm visiting Berkeley University during the month of April. During my visit I'm giving 4 lectures on termination proving. Here are the slides. Warning: they're around 20mb each.

Roger Needham award

I won the Roger Needham award. Thanks to those who nominated me, the committee, and those who were asked to write letters.............whoever you are.

Interesting termination bug

Perhaps you heard about the Zune leap year bug? Sort of an interesting bug. This is a classic example of a liveness/termination bug, as explained here. And yes..... TERMINATOR can find this bug.....

SF weekly

SF Weekly makes note of the Vogue article.