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.

Termination research now VERY fashionable ;-)

I'm mentioned in Vogue in an article about Tauba. Dec '08....the year termination research become fashionable ;-)

no kidding, functional programming has really arrived.....

Watching this talk gave me shivers. My love (functional programming) is now mainstream. Very funny talk, by the way.

Eric Koskinen

Welcome to Eric Koskinen, who just started his PhD at Cambridge University under the supervision of myself and Matthew Parkinson.

Professor Cook

Queen Mary, University of London has now appointed me as full professor of computer science. I'm not leaving Microsoft, of course, its a joint appointment with Microsoft Research.

methods of proving recursive programs terminating

I'll state this perhaps a bit too strongly (to make the point). Recursion, and program termination, are completely orthoginal issues. Check out our new paper: CFL-Termination. This paper shows you how (if you have an oracle for partial correctness semantics) you can convert recursive programs into semantically equiv. non-recursive programs without tricky encodings using heap or non-linear updates to arithmetic variables. Enjoy ;-)

F# release

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

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.

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.......