Byron Cook

New papers on liveness proving

2011-06-04T04:06:00.000-07:00

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

Kinect

2010-11-23T02:01:00.000-08:00

Here's a nice article on Kinect and the work at MSR-Cambridge behind it.

New papers

2010-11-03T03:37:00.000-07:00

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:

Making prophecies with decision predicates, with Eric Koskinen. This will appear
at POPL'11
Proving stabilization of biological systems, with Jasmin Fisher, Elzbieta Krepska, and Nir Piterman. This will appear at VMCAI'11

Congrats to Andrey Rybalchenko!

2010-09-06T04:00:00.000-07:00

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

2009-10-07T03:18:00.001-07:00

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

Healthcare reform article

2009-08-16T14:14:00.000-07:00

An article in the Guardian by Bee: American healthcare is in truth already rationed

Congrats to Viktor Vafeiadis

2009-06-18T03:40:00.000-07:00

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

A new look at hardware synthesis

2009-06-15T01:56:00.000-07:00

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

2009-04-06T07:53:00.000-07:00

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

2009-03-25T05:03:00.000-07:00

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

2009-01-02T07:39:00.000-08:00

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

2008-12-30T17:13:00.001-08:00

SF Weekly makes note of the Vogue article.

Termination research now VERY fashionable ;-)

2008-12-29T12:50:00.000-08:00

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

2008-11-01T09:36:00.001-07:00

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

Eric Koskinen

2008-10-28T11:50:00.000-07:00

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

Professor Cook

2008-10-28T11:47:00.000-07:00

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

2008-10-28T11:44:00.000-07:00

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

2008-08-31T07:35:00.000-07:00

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

British pastimes...

2008-08-20T06:28:00.000-07:00

cheers!

vacation.....actionscript

2008-08-08T15:18:00.001-07:00

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

2008-07-28T00:43:00.000-07:00

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

Balance.....

2008-07-24T09:03:00.000-07:00

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

2008-07-23T11:43:00.000-07:00

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

2008-06-03T23:24:00.001-07:00

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"

2008-06-02T02:49:00.001-07:00

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

Imperial lectures, details.......

2008-05-23T15:31:00.000-07:00

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!

2008-05-19T01:36:00.000-07:00

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

2008-05-19T01:33:00.000-07:00

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

Off to Oxford, then MPI

2008-05-02T06:00:00.000-07:00

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

Concurrency.....

2008-04-29T03:16:00.001-07:00

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

A long time coming.....

2008-04-28T03:08:00.000-07:00

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

2008-04-08T07:30:00.000-07:00

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

Great films

2008-04-07T00:53:00.000-07:00

I've seen a couple of really great films recently:

Go see them!

CAV papers......

2008-04-02T13:33:00.000-07:00

I co-authored a couple of papers that will appear at this year's CAV conference:

Proving Conditional Termination, with Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
Scalable Shape Analysis for Systems Code, with the East London Massive

The young folks......

2008-03-22T06:24:00.000-07:00

My youngsters are storming the web with content........see Mina and Aubrey.

Terminator at Techfest keynote speech

2008-03-20T05:44:00.000-07:00

Rick Rashid (Senior VP of Microsoft Research) discusses Terminator, termination, and liveness in his TechFest keynote address. See the video (at 29m into the talk).

Imperial lectures

2008-03-13T07:56:00.000-07:00

I'll be giving a mini-course on proving program termination/liveness at Imperial, May 26th, 27th, and 28th, from 2-4pm. If you're in the London area you're welcome to come, to send students, etc. These lectures will be a condensed version of the 14 lectures on the same topic that I gave at Carnegie Mellon this winter, and preliminary version of what I will give at Marktoberdorf this summer.

Final week at CMU, returning to Cambridge

2008-03-01T22:31:00.000-08:00

This is my final week at CMU. On wednesday I go to Baltimore to attend the NSA's HCSS meeting (where I will give a talk and sit on a panel), and then I return to Cambridge.

My visit to CMU was fantastic. Thanks to Ed Clarke, Jeannette Wing and Randy Bryant for the invitation, and to Peter Lee, Randy Bryant, and Denny Marous for making it happen. I worked with a number of great people, learned a lot, and made many new connections. It was an exciting time to be at CMU, especially given the recent announcement about this year's Turing prize winners.

My course seemed to go remarkably well, especially considering the lack of introductory papers/books from which to draw material. I can confidently assert that my course was the most in-depth course on termination/liveness ever taught before......with 14 lectures covering topics such as well-founded relations, decomposition techniques, rank function synthesis, invariance and variance analysis, refinement, inductive proof techniques for termination, termination for recursive and concurrent programs, and fair termination. Throughout the course I had numerous bright people in the audience asking questions and participating in discussion. Special thanks to the core group (those that attended nearly all of the lectures): Stephen Brooks, Sager Chaki, James Ezick, Arie Gurfinkel, Will Kleiber, Neel Krishnaswami, Stephen Magill, Sean McLaughlin, Frank Pfenning, John Reynolds, Robert Simmons, Jiri Simsa, Michael Tschantz, and Kwangkeun Yi.

Note: Upon hearing about my course at CMU, several people outside of CMU have asked for copies of notes and/or slides. I am currently preparing a more polished version of the notes, please contact me if you would like to see a draft when I'm happy with it........

F# team is hiring

2008-01-30T11:33:00.000-08:00

--------------------------------------------------------------------------------
From: Don Syme
Sent: Wednesday, January 30, 2008 7:29 PM
To: FSharp Discussion
Cc: Programming Languages Interest Group
Subject: The F# team is hiring!

Hi all,

The F# team continue to have a number of positions open for compiler and language tools experts. Positions are by default in Redmond.

If you're interested in helping to bring a typed functional programming language into Visual Studio and think you have skills and commitment relevant to the achieving this, then please contact me or another member of the F# team to see if there might be a fit. If there's no immediate fit, then there may be one later, so don't be shy. We're looking for compiler experts, including optimization, type checking, performance and correctness language tools experts, e.g. experienced with language services and Visual Studio language tools QA/test experts

Kind regards

Don

Pittsburgh: the friendliest town ever?

2008-01-25T22:44:00.000-08:00

I travel a great deal. Some cities will remain legendary in my mind for their hospitality during my frequent visits. Cities deserving extra special mention include NYC, Baltimore, Paris, Seattle, SF. Other cities are HORRIBLE to visit. San Diego comes to mind (sorry, nice weather, but "pass!"). Edinburgh is pretty but (based on 3 or 4 trips that I've made thus far) emotionally cold.

I've been happily surprised at the level of hospitality that I've encountered here in Pittsburgh. Many CMU people have invited me out to dinner, or to their homes. Old friends who now live in Pittsburgh have taken me out to shows, bars, etc. Tonight I had many social invitations: a concert, a dinner, etc. I'd already made plans to hang out with Lli (old Portland friend since 1996?). Tonight was the "gallery crawl" in downtown Pittsburgh, Lli and I ended up spending our entire gallery crawl time at this gallery. We also drove around a bit and talked, and went to dinner.

All settled in at CMU

2008-01-22T14:16:00.000-08:00

For the past week I’ve been settling in at CMU. I’m teaching a graduate course on termination (and writing some companion lecture notes). I've been meeting with the many smart professors/students/researchers. I'm also working on several papers.

For the first few days I stayed in John Reynolds’ amazing house. Then I found my own place. The neighbourhoods here are great, and the houses are HUGE by my UK/Seattle standards.

I have a great office which rivals the office I have at MSR-Cambridge, with a great view!

PhD students: its time to apply for the Marktoberdorf summer school

2008-01-19T03:15:00.000-08:00

Note: its now time to apply to attend Marktoberdorf.

Teen pregnancy a good thing?

2007-12-27T09:08:00.000-08:00

You might turn a little bit pro teen pregnancy if you read Bee's article which appeared in the Guardian. Congratulations to Bee, as the Guardian has picked this article as one of its best articles of the year.

PS. Happy holidays from snowy Colorado!

En route to San Francisco/Colorado/CMU

2007-12-16T15:45:00.000-08:00

I'm flying in the morning to San Francisco. I'll spend christmas in Colorado with my family, and then return to San Francisco for POPL. After POPL I'm going to CMU for my sabbatical.

text-only web browsing!

2007-12-12T03:30:00.000-08:00

Last night at dinner with Bee and Josh, we discovered our shared mutual love for text-only web browsers like Lynx. Furthermore: Josh and I happily learned that we are not alone in our frequent use of Lynx in effort to cut out the cruft of the web.

Trends in concurrency summer school

2007-12-10T04:49:00.000-08:00

PhD students: I'm teaching at the Trends in Concurrency summer school in Prague. Be sure to apply for a spot, as space will be very limited.

Marktoberdorf summer school

2007-12-09T14:58:00.000-08:00

PhD students: I will be teaching at Marktoberdorf this summer. The list of lecturers has been announced, and the application process will open soon. Be sure to apply soon as space will be limited.

SLAM/SDV rule kit now available!

2007-12-07T08:23:00.000-08:00

The Static Driver Verifier (SDV) Rule Development Kit (RDK) is now available. The RDK is an extension to SDV that allows you to adapt SDV to support additional frameworks (or APIs) and write custom SLIC rules for this framework. The goal of the RDK is to allow researchers to experiment with writing SLIC rules for APIs and to gain experience using the SLAM verification engine that underlies SDV. To request a copy of the RDK, please e-mail rdk_req@microsoft.com

Ranking abstractions

2007-12-07T05:12:00.000-08:00

Our paper entitled "Ranking abstractions" will appear at ESOP'08. Here's the submitted draft, a final version is in preparation.

Postdocs, interns, apply now

2007-11-30T06:37:00.001-08:00

As of writing this the MSR admins have yet to update the page http://research.microsoft.com/aboutmsr/labs/cambridge/postdoc.aspx , but I know that we are planning to hire some postdocs in FV/PL this coming year. We also have slots available for interns, see http://research.microsoft.com/aboutmsr/jobs/internships/about_uk.aspx.

If you want one of these positions you should be getting your materials together now (letters of recommendation, etc). Also: please don't just formally apply on the website without sending me some mail letting me know that you've applied.

Shape analysis, for real!

2007-11-30T05:47:00.001-08:00

Those of you involved in automatic program verification should take notice of this paper:

On Scalable Shape Analysis
Authored by Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano, Peter O'Hearn

Sad days.....

2007-11-30T03:51:00.000-08:00

As some of you may know.......although I dont live in Seattle....since moving to europe I somehow have ended up spending lots of evenings and early mornings on the 500 block of E. Pine in Seattle. Perhaps I averaged 1/8 weekends there? Amazing. Well. That era is over, as its getting ripped down for progress. Time to grow up I suppose, or find some new good Seattle bars.

Comings and goings.....

2007-11-29T15:03:00.000-08:00

Happy post thanksgiving. Some notes:

I've been invited to speak at the CAV'08 workshop on numerical abstractions.
Tal Lev-Ami and Mooly Sagiv visited last week, and kept me busy with a research topic that we've been working on for some time but only recently began to understand.
John Reynolds' visit is over and he is now returning back to Carnegie Mellon.
I'll be in San Francisco and Denver from Dec 18th until Jan 12th
On Jan 12th I'm going to Carnegie Mellon for my sabbatical

Old blog (April '02 through Nov '07)

2007-11-26T04:08:00.000-08:00

- November 2007 -

Congratulations to Viktor Vafeiadis, who successfully completed his PhD this month. Starting in January, Viktor will start his postdoc with me here at MSR-Cambridge.

I first met Don Syme in 1997 when he and I were both interns at Intel's Strategic CAD Labs. He and I drove together to work every day from Portland and fast became friends. We are still friends today---our offices are even next door to each other. Don is, in fact, the reason that I moved to Cambridge. At Intel Don worked on formal verification and decision procedures and I worked on advanced functional programming language topics (lazy evaluation, parametricity, etc). We both ended up going to Microsoft's research division instead of Intel's, where---strangely---we've traded research topics. At Microsoft Research Don helped bring generics to the world of industrial programmers, while I helped bring automatic program verification to the world of industrial programmers via SDV and SLAM (which led to TERMINATOR, which led to SLAyer). During the SLAM days I wrote Microsoft's first decision procedure tool called Zapato (which led to Madan's Zap and now Nikolaj and Leonardo's Z3 product). Don's work on generics has since led to a new product called F#.

The other day I wanted to write a new implementation of the rank function synthesis engine used within TERMINATOR. After some investigation I decided that the best way to do this was to use the confluence of tools that I've been directly and indirectly involved in for 10 years (F#, Z3, etc). As John Reynolds said when I showed him the code: "It's amazing how all of this work and these ideas have come together so nicely". Are you interested in knowing more? Then read this, where I make a ~200 line F#/Z3 application that implements TERMINATOR's rank function synthesis procedure.

CMU-folks: you should sign up for my course on program termination.

I visited the NASA Ames research center in the bay area this month. I also visited with several product groups at Microsoft in the Seattle area.

I worked together with Andreas Podelski and Andrey Rybalchenko for a few days in Paris.

- October 2007 -

S. Somasegar (Corporate VP of developer tools,etc at Microsoft) says some very strong words about F#, functional programming, Don Syme, and Microsoft Research. A real highlight is:

"This is one of the best things that has happened at Microsoft ever since we created Microsoft Research over 15 years ago. Here is another great example of technology transfer at work. We will be partnering with Don Syme and others in Microsoft Research to fully integrate the F# language into Visual Studio and continue innovating and evolving F#."

Don's blog also has some interesting things to say about the new level of investment in F# at Microsoft.

Here's a pointer to a paper that we've submitted to ESOP'08 for review:

Ranking abstractions
A. Chawdhary, B. Cook, S. Gulwani, M. Sagiv, and H. Yang
Submitted to ESOP'08

I'm teaching a mini-course this month at Cambridge University on proving program termination. October 15th, 19th, and 22nd. 10am-12pm, Gates Building Room FW11. Here are the slides from the course:

In addition to teaching at the Marktoberdorf this coming summer, I've also decided to accept the offer to teach at the International Summer School on Trends in Concurrency.

- September 2007 -

Here's another interview with me about TERMINATOR.

By the way: have you just recently finished your PhD? Do you need a job as a postdoc working on program verification at Cambridge?

Or maybe you're looking for an development position with the SDV/SLAM team?

Some professional notes:

I've been asked to give a presentation to Bill Gates and other Microsoft executives about TERMINATOR.
I, together with Tayssir Touili, have been asked to co-chair CAV'10. CAV'10 will be a FLoC'10 conference in Edinburgh.
Viktor Vafeiadis has joined me here at MSR-Cambridge as a postdoctoral researcher.
John Reynolds is visiting me here at MSR-Cambridge for 3 months.

- August 2007 -

August was a blur of reading POPL submisions. I spent almost all of August in Seattle/Redmond, where I sat either in Tom Ball's office, borrowed desk space at my friend Anika's company, or cafes such as Zeitgeist or Top Pot.

I left Seattle once during August to be the external examiner at Daron Vroon's PhD dissertation defense at Georgia Tech. Congratulations to Daron for a job well done!

A couple of professional notes:

We had a paper accepted for publication:
Local reasoning for storable locks and threads
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv
To appear: APLAS'07 [Asian Symposium on Programming Languages and Systems] (Singapore)
I was asked to serve as the workshop's chair at CAV'08 in Princeton, NJ.

- July 2007 -

The slides from my CAV invited talk can be found here.

Click here to watch an interview with me from channel9.msdn.com.

As of this month I've been in Cambridge for 3 years, and on August 5th I will celebrate my 5th year at Microsoft. Additionally, my lab is celebrating its 10 year anniversary.

I'm now preparing myself for the task of reviewing 30+ POPL papers. It looks like I'll lose much of my August. ;-)

At the end of this month I will be in the US for the remainder of the summer. Before I go to the US, however, I will host visits by Nikolaj Bjorner, Leonardo de Moura, and Amir Pnueli.

Unfortunately I will be out of town at the time, but If you're into this sort of thing, you should go to SeparationFest.

Check out the following draft paper:

Local reasoning for storable locks and threads
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv

I was invited to give a talk in the "Five Things I Wished I Learned In College" session at QCon.

Oh, and take a look at my new favorite website. ;-)

- June 2007 -

Note that the POPL'08 submission deadline (July 16th) is getting close!

I've just returned from a trip to the US, where I visited Ken McMillan in Berkeley, gave a talk at PLDI in San Diego, and worked with Sumit Gulwani and Mooly Sagiv in Seattle.

- May 2007 -

I'm giving a set of tutorial lectures on proving program termination at the NSA's High Confidence Systems and Software conference this month in Maryland. While I'm in the US I'm also visiting Cornell. Later in the month I will return to Nice to give an invited lecture at MEMOCODE.

In matters of money, congrats to Andrey Rybalchenko, Dino Distefano, and Hongseok Yang:

Dino Distefano has been awarded a 5 year fellowship from the UK Royal Academy of Engineering.
Andrey Rybalchenko is awarded 250,000 euros (oh, and a laptop) for his future research from the MSR European Fellowship Program.
Hongseok Yang was awarded a 5-year EPSRC fellowship.

A few papers that I've co-authored were recently accepted for publication:

Arithmetic strengthening for shape analysis
Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.
To appear: SAS'07 [International Static Analysis Symposium] (Denmark)
Proving termination by divergence
Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric
To appear: SEFM'07 [International Conference on Software Engineering and Formal Methods] (London)

Oh, and the new book Developing Drivers with the Windows Driver Foundation has a chapter about SLAM/SDV.
My new dutch bike!

- April 2007 -

You can watch the talk that I gave at TechFest'07: Automatically Proving Concurrent Programs Correct

I'm in the US for much of April.

The paper we submitted to CAV'07 was accepted for publication:

Shape analysis for composite data structures
J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang
CAV'07 [International Conference on Computer-Aided Verification] (Berlin)
Here's a pointer to the submitted version (The final version will be done in late April)

- March 2007 -

People threw birthday parties for me in both Cambridge and London. I feel very loved. Here are some picture from the London party, including sightings of the best gift i've receieved in years (the little Byron from the Yangs)

It's been a big month for Bee:

Listen to Bee interviewed on the BBC Radio 4 program Midweek.
In her lifetime Bee has largely only recieved positive reviews of her work in the press (some highlights include an amazing review in the New Yorker for her website and the review in Time Out NYC for Lessons in Taxidermy). But I've never seen a review that truly understood Bee and her current book as much as the one that appeared in the March 18 edition of the Sunday Telegraph. I can't find the review online, but here are some memorable quotes:
- It is this juxtaposition of sparse, elegant language and acceptance of larger unexplainable forces in her life that gives this memoir its power
- It is one of the many charms of this book that Lavender is not only aware of the conventions of such autobiographies but that she conciously rejects them
- Narrative is as important as beautiful writing and Lessons in Taxidermy drives the reader on to the next chapter
- Her powerful, elegant memoir should be read by everyone .... as an example of what truly well-written and unflinching self-examination can be like.
Many congratulations to Bee and her wonderful book that comes out today (March 21st) in the UK!

- February 2007 -

Photo from my most recent US lecture tour

Some notes:

I was invited to be a lecturer at the Marktoberdorf summer school in the summer of 2008.
I'm giving a colloquium lecture at Harvard on March 1st
I'm speaking at MIT on February 28th.
I will be in Seattle/Redmond in early March for Microsoft's TechFest, where I'm giving a lecture.
I'm visiting the Models and Theory of Computation group at EPFL in February, where I will be Ashutosh Gupta's external examiner.
I will be an invited speaker at MEMOCODE'07 in Nice.
I will be an invited speaker at SEFM'07 in London.
I was invited to be a member of the POPL'08 program committee
I will be teaching a mini-course on proving program termination at Cambridge University in the Autumn (Oct 15th, 19th, 22nd. 10am-12pm, Gates Building Room FW11).
Here is another interesting Scientific American article about MSR.

- January 2007 -

Two of my papers were accepted for publication at PLDI'07:

Proving thread termination
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
To appear: PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)
Thread-modular shape analysis
Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv
To appear: PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

Are you interested in knowing more about how to automatically verify properties about the data-structures used in programs? Then you should attend the International Symposium on Automatic Heap Analysis on July 2nd in Berlin (the day before CAV).

I'm now back from a week in London and a week in Nice for POPL and VMCAI. I'm now preparing for a number of visitors (including Sumit Gulwani, Mooly Sagiv, Noam Rinetzky, and Helmut Veith). Greta Yorsh begins her internship here at MSR-Cambridge in February.

Josh and Hongseok

- December 2006 -

Perhaps I needed a break. I got one. Things started off well in early December with a productive trip to San Francisco/Berkeley, where I worked for several days with Ken McMillan. In Seattle my work plans were killed by a historic windstorm that took out electricity for much of western Washington and Oregon (including Microsoft). I took several days off in Colorado with the intention of returning back to the UK to work on several papers. This time a historic blizzard (3 feet of snow!) closed the Denver airport for days, while fog in London closed Heathrow for days. My flight was cancelled and then rescheduled for a flight 7 days after my original flight!. Happy new year.

- November 2006 -

There's an article about TERMINATOR in the December issue of Scientific American entitled Send in the Terminator. You cannot read the full article unless you buy the magazine. However, here are the first two paragraphs.

Another article about TERMINATOR appeared in the Nov. 22nd edition of the Financial Times. The online version of the article costs money.

- October 2006 -

I show up in a comic that Dino put up on his SpaceInvader blog.

The VMCAI'07 list of accepted papers has been released.

If you're into decision procedures,etc you should submit a paper for publication in the Special Issue on Satisfiability Modulo Theories that I am co-editing with Roberto Sebastini for the Journal on Satisfiability, Boolean Modeling and Computation.

Ganesan Ramalingam (a.k.a. Rama) dropped by and visited our group for a week. Andreas Podelski and Andrey Rybalchenko dropped in recently. We've also had many recent visits from the likes of Dino Distefano, Peter O'Hearn and Hongseok Yang.

- September 2006 -

Some professional news:

I will be an invited speaker at CAV'07.
Two papers that I've co-authored will appear at POPL'07:
Proving that programs eventually do something good
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi
To appear: POPL'07 [Symposium on Principles of Programming Languages] (Nice)
Variance analyses from invariance analyses
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn
To appear: POPL'07 [Symposium on Principles of Programming Languages] (Nice)
A paper that I co-authored will appear in the Journal of Logical Methods in Computer Science:
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu Lahiri, Thomas Ball and Byron Cook
To appear: Journal of Logical Methods in Computer Science

Richard Bornat and I in a "friendly argument" about logic

Mooly Sagiv has arrived in Cambridge for his 3-month visit to our lab. Josh and I also have two interns who've arrived in the past few weeks: Alexey Gotsman, Thomas Wies.

Oh, and I've just returned from Strasbourg, where I've been working with Andreas Podelski and Andrey Rybalchenko. We've got a really great new idea. More later!

I'm giving a couple of departmental seminars in the near future: One at Queen Mary, University of London and one at Cambridge University.

- August 2006 -

I'm finally back from my tour of the American west coast. During my trip I gave 12 lectures (at Stanford, Berkeley, two lectures at Intel Research, SRI, Microsoft Reserch, four lectures a FLoC, etc). By far the best question during my lectures occured at Stanford, where someone asked "can TERMINATOR prove the termination of my 91 function?" I think that it probably looked like I kept my cool, but inside my head I was thinking oh my god, that's John McCarthy!

Microsoft's research division has put up an article about TERMINATOR on their website.

- July 2006 -

Hello from Seattle. Ive been on a bit of a whirlwind trip during the past couple of weeks across the west coast of the US: Ive visited Intel-Oregon, Intel in Santa Clara, SRI, Berkeley, Stanford, MSR-SVC, MSR-Redmond, Galois, PSU, and OGI. I'm now moving into a temporary apartment in Seattle before the start of FLoC.

- June 2006 -

I've been working recently on a method that converts invariance property generators into termination analyses. I'll be speaking about this new work when appearing as the invited speaker at the International Workshop on Termination at FLoC:

Title: Program termination analyses for free!
Abstract: I will describe an easy-to-follow recipe for the construction of automatic program termination analyses. The recipe's primary ingredient is an abstract-interpretation-based program analysis for invariance properties - any one will do. If we change the underlying program analysis, we get a different program termination analysis.

The SSPV schedule is now available. Also, we have now released the list of PDPAR's accepted papers and PDPAR's schedule.

Stephen Magill has now begun his internship with me in Cambridge. Note that I've recently put up some notes about doing internships with me.

Both Helmut Veith and Kousha Etessami have recently made appearances at my lab. I feel very fortunate to be near the Newton Institute, as it draws in many additional smart short-term visitors like these to Cambridge.

In July I will be at the Challenge of Software Verification seminar at Dagstuhl. I am also going to Barcelona for Albert Oliveras' dissertation defense.

Late in July we are moving operations to the US until September.

Several articles that we've submitted to conferences were recently accepted for publication:

Interprocedural Shape Analysis with Separated Heap Abstractions
Alexey Gotsman, Josh Berdine, and Byron Cook
SAS'06 [International Static Analysis Symposium] (Seoul)
Over-Approximating Boolean Programs with Unbounded Thread Creation
Byron Cook, Daniel Kroening, Natasha Sharygina
FMCAD'06 [Formal Methods in Computer Aided Design] (San Jose)

- May 2006 -

TERMINATOR and TERMINATOR in Cambridge's midsummer common.

Here's information about the upcoming VMCAI'07. Be sure to submit a paper!

I will make another appearance as a guest lecturer at Mike Gordon's course on Specification and Verification next door at the Cambridge Computer Science department later this month.

It's probably time to start planning your FLoC travel. Be sure to get to FLoC by the morning of August 10th so that you can attend the Symposium on Satisfiability Solvers and Program Verification (SSPV)!

While I'm on the subject of FLoC let me also help you plan your workshop/conference attendence so as to maximize your Byron-time ;-)

Choose SSPV as your pre-conference event,
Choose the Workshop on Termination (WST) as your mid-conference workshop, as I will be giving an invited lecture,
Go to the Computer-Aided Verification (CAV) conference, as I will be giving at least one and perhaps two talks there.
In the post-conference workshops you're going to have to spread yourself thin:
- You'll need to attend the part of the Workshop on Software Verification and Validation (SVV) when I am giving my invited lecture,
- You'll then need to shift rooms over to either Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) (which I am co-organizing) or Threads Verification (TV) (of which I am a member of the PC) .

I will also be visiting the Microsoft headquarters before and after FLoC.

Good news: Jacopo Mantovani is interning with me here at the lab for three months. Bad news: Georg Weissenbacher must now return to Zurich to resume his PhD studies.

Microsoft's Windows division has put up a couple of articles about Static Driver Verifier that will appear in the proceedings of its WinHEC conference:

- April 2006 -

My blog (of sorts...) is now 4 years old.

I will be an invited speaker at the International Workshop on Termination (WST'06) at FLoC, where I will presumably speak about aspects related to TERMINATOR.

Uh oh..... two of my worlds are going to collide! Portland indie-rock-block is coming to London in full force!

I'm spending much of this month away from Cambridge. I am giving an invited talk at the Workshop on Automated Reasoning in Bristol. I am taking some time off and going to Bath. I am giving a talk at EuroSys in Leuven. Then I'm flying to the US where I will be a member of a formal methods panel discussion at the University of Illinois Urbana-Champaign Affiliates Conference. While in the US I will also visit Carnegie Mellon for a few days. Then I'm off to Switzerland to attend the Alpine Verification Meeting.

Three articles that I co-authored will appear at this year's CAV. The first is a TERMINATOR-related article about MUTANT, the idea that I've been alluding to for some time in this blog:

Automatic termination proofs for programs with shape-shifting heaps
Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

We also have a short TERMINATOR tool description paper:

Terminator: Beyond Safety (short tool description)
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Finally, we have a paper about a semi-automatic method of fixing bugs found with SLAM-like software model checkers

Repair of Boolean Programs with an Application to C
Andreas Griesmayer, Roderick Bloem, and Byron Cook
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

- March 2006 -

This is a month of many visitors: Georg Weissenbacher is interning with me for three months, Daniel Kroening is visiting me for 2 weeks, Arie Gurfinkle is visiting for a few days, and Viktor Kuncak is also planning a stop-over on his way elsewhere in Europe. Peter O'Hearn and Moshe Vardi have been here for a while as they are both 6 month visitors to the lab. Others rumoured to be visiting include Dino Distefano, Shuvendu Lahiri, Andreas Podelski, Andrey Rybalchenko. and Hongseok Yang.

I was asked to be an invited speaker at AVoCS 2006 in France.

In addition to my positions at Microsoft Research and Chalmers, I'm now a visiting professor at Queen Mary, University of London.

Also, I'm co-organizing a FLoC symposium on satisfiability solvers and program verification together with Dimitris Achlioptas and Moshe Vardi. The workshop will be held on August 10th and 11th in Seattle. It's being funded by the Institute for Pure and Applied Mathematics (IPAM). The speakers will be

We've finished working on the final version of our PLDI paper:

Termination Proofs for Systems Code
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)

Additionally, our EuroSys paper on SDV and SLAM is ready:

Thorough Static Analysis of Device Drivers
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner
EuroSys'06 [European Systems Conference] (Leuven)

- February 2006 -

Greetings from Seattle.

Here are some slides and audio from a seminar that I gave at the Isaac Newton Institute for Mathematical Sciences in Cambridge.

I'm trying to hire someone as a programmer for the TERMINATOR project. Here's more information.

Back in November I had a nifty idea while on the train to London to meet with the East London Massive---a method of proving the termination of imperative loops that modify the shape of the heap (here are some pictures of that meeting). We're working on the details and implementation now---we're calling the implementation MUTANT. Here are some photographs from our latest meeting at Peter's house.

I was asked to be the invited speaker at the International Workshop on Software Verification and Validation at FLoC'06 in Seattle. In other FLoC'06-related news: Koen Claessen and Peter O'Hearn accepted our invitations to speak at PDPAR'06.

I went home to Colorado this month to see my parents and old friends,etc. While there, of course, I couldn't help but stop in and visit Fabio Somenzi's group. I gave a talk about TERMINATOR and MUTANT.

Just before going to Colorado I visited Joel Ouaknine at Oxford, where I gave a seminar and was taken to a fabulous dinner (with unbelievable amounts of wine!) at St. Johns college. My visits to Oxford are never dull!

- January 2006 -

Bee's book (Lessons in Taxidermy) has made a number of best of the year type lists, including Time Out Chicago's top ten and the American Library Association's best books list.

Both Peter O'Hearn and Moshe Vardi have joined our lab as visiting researchers. In addition, Andrey Rybalchenko and Dino Distefano are visiting for several weeks.

An article about TERMINATOR that I co-authored with Andrey and Andreas was accepted for publication at PLDI:

Termination Proofs for Systems Code
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)

Also: another article that I co-authored about SDV and SLAM was accepted for publication at EuroSys:

Thorough Static Analysis of Device Drivers
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner
EuroSys'06 [European Systems Conference] (Leuven)

The intention of this paper is to provide a single comprehensive paper on SLAM and SDV that most people in computer science should be able to understand. It demonstrates a real bug found with the tool, and describes the outcome of SDV on a large number of device drivers. I'm working on the final versions of both of these papers and will put up PDFs when I'm done.

On a related note, here's an interesting article from the Register: Windows beats Linux / Unix on vulnerabilities.

I attended the Chalmers Winter Meeting this month in Sweden. I sat in on a number of great technical lectures. I especially enjoyed the talk by Oskar Sanberg on dark nets. There was also some late-night sauna and beer-drinking. I will go back to Sweden soon to give a lecture in a course on formal methods and speak at the next FM meeting.

I'm giving a seminar talk on Feb.3 at the Newton Institute for Mathematical Sciences. I'm also due to give a seminar at the University of Edinburgh on March 21st.

Andreas and I will co-chair the next VMCAI in 2007.

- December 2005 -

I've taken a bit of time off work for the holidays. I haven't really gone anywhere but instead played with my children and read back issues of the New Yorker magazine. Oh, and I've been to lots of parties: christmas parties, going-away parties, birthday parties,etc.

Check out Smallfoot, which comes from The East London Massive.

- November 2005 -

TERMINATOR, the project that I've been working on with Andreas and Andrey, now has a website.

TERMINATOR has been hanging out with the East London Massive some recently. Dino visited Andreas and Andrey earlier this week. Then I went down to London (here are a few pictures).

Josh Berdine is taking a job with us here at the Cambridge lab this month (here is his new webpage). Also: Peter O'Hearn is visiting for 6 months, starting in January.

I've just returned from a trip to the US and Canada, where I gave several talks about TERMINATOR at the University of Toronto, New York University and the the National Security Agency in Maryland.

There's a new article about SLAM and Static Driver Verifier (SDV) on www.wired.com.

- October 2005 -

I went to Paris this month for more meetings at Le Rostand with Andreas and Andrey. I took the train back on Halloween night, just in time to escape the French riots. Andreas and Andrey are now coming to Cambridge. We have some writing and programming to do.

Our friend Marisa Anderson is coming to Cambridge for thanksgiving.

I have been asked to give an invited talk at the Workshop on Automated Reasoning in April.

- September 2005 -

Earlier this month I went to Seattle, where I gave a talk at MSR/Redmond, and worked with my colleagues there. I also visited Domagoj Babic and Alan Hu at the University of British Columbia in Vancouver,BC.

Congratulations to Georg Weissenbacher (w/ Prof. Daniel Kroening), Aziem Chawdhary (w/ Prof. Peter O'Hearn), Loic Fejoz (w/ Prof. Stephan Merz), and others for winning Microsoft Research PhD scholarships.

In other professional news:

Roberto Sebastiani and I are going to organize the 2006 PDPAR workshop at FLoC in Seattle.
I have also agreed to be on the TV'06 program committee, which will also be at FLoC.
I will be on the program committee and serve as the tool chair at TACAS'07 in Portugal.
I'm giving an invited talk at the International Computer Science Symposium in Russia (St. Petersburg)

While in Seattle I also had time to go out with my friends. I was extremely fortunate to have been at Seattle's bus stop bar when this happened.

- August 2005 -

I went to San Francisco this month to give a talk at SPIN'05. I was only there for 3 or 4 days, but I managed to go to several fabulous dinner parties with old friends, and to a huge party in Sonoma hosted by Jonathan and Hiya. I slept that night in Sonoma and went to the river with Jonathan, Hiya, and their friends. I returned to Cambridge just in time for a visit by John Matthews and Andrey's end-of-internship talk.

I've been working with Georges Gonthier on a technical result about Stalmarck's algorithm. We've written up an article about it:

Using Stalmarck's algorithm to prove inequalities
Byron Cook, Georges Gonthier
ICFEM'05 [International Conference on Formal Engineering Methods]

If you live here in the UK then you know that the UK and London are extremely expensive places to be/visit. My fantastic friend Chloe (who owns and runs reading frenzy) would like to visit. It's a good cause (more info here). If you live in the London area then you should go to this nifty fundraising event.

- July 2005 -

In addition to my work at Microsoft Research, I've accepted an offer to be an Associate Faculty in the Chalmers computer science department and the formal methods group.

Speaking of Chalmers and the formal methods group: Congratulations to by Niklas Eén and Niklas Sörensson, the authors of MiniSAT. MiniSAT beat the competition at SAT 2005. Furthermore, they did it in style: MiniSAT is less than about 2000 lines of extremely clear C++ code (this 2000 lines includes empty lines and comments). This is a real contribution. Niklas Sörensson gave a great invited talk at ESCAR on MiniSAT.

Andreas Podelski is visiting me for three months in Cambridge.

- June 2005 -

Bee's book was nominated for a Quill award and an ALA award!

I've just returned from Seattle, where I organized a Microsoft-internal meeting on decision procedures, theorem provers, and constraint solvers. I also met with with a number of researchers and developers in Redmond. Jakob Lichtenberg and I worked quite a bit on improving the performance of SLAM when compiled with F#.

Andrey Rybalchenko started his internship here at the lab with me.

I will be sitting on a panel discussion with Robert Kurshan, Constance Heitmeyer and John O'Leary at MEMOCODE in Verona.

I will also be attending CAV and the Software Model Checking workshop. A hoard of folks are visiting me here at the lab before CAV. These include Domagoj Babic, Tom Ball, Daniel Kroening, Natasha Sharygina, Cesare Tinelli, Greta Yorsh, and Lintao Zhang.

I'll be travelling to Tallinn to attend CADE. I am giving an invited talk at the CADE workshops ESCAR and Disproving. I will also be on a panel at ESCAR.

- May 2005 -

Check it out! The Village Voice reports that Bee is a best seller.

A couple of articles that I have co-authored have been accepted for publication. One at SPIN, and the other at SAS:

Abstraction-refinement for termination
Byron Cook, Andreas Podelski, Andrey Rybalchenko
SAS'05 [International Static Analysis Symposium] (London)
Symbolic model checking for asynchronous Boolean programs
Byron Cook, Daniel Kroening, Natasha Sharygina
SPIN'05 [International SPIN Workshop on Model Checking of Software] (San Francisco)

I gave a guest lecture across the street in Mike Gordon's course on specification and verification.

Here's an interesting bit of news about Microsoft and licensing of research.

Georges made the article he's written about his 4-colour theorem proof available.

This would be an interesting job. Galois is a company started and staffed almost entirely by my old OGI-based Haskell entourage.

- April 2005 -

Recent work-related news:

A beta release of Static Driver Verifer / SLAM---the tool that I co-developed with people in Microsoft Research and the Windows division---is now publically available (for free....). Look here for more information.
In related news (SLAM is written in INRIA's programming language Caml), Microsoft joined the Caml consortium.
Coincidentally, Microsoft also announced that Microsoft Research and INRIA are opening a laboratoire commun in France.

I've just returned from ETAPS in Edinburgh. While there I chatted with many of my friends and colleagues, and met some new people too. There were some good talks. Since we have so many visitors at Microsoft Research I have often already seen extended versions of these conference talks, or have already spoken to the researchers about their work. One impressive talk that I knew absolutely nothing about beforehand was Jesse Bingham's talk entitled Empirically Efficient Verification for a Class of Infinite-State Systems. I haven't read it yet, but here's a pointer to an extended version of the article. As one might expect, Rustan Leino also gave a fantastic talk. He described a method of supporting nested quantifiers in a prover that implements lazy abstraction of first-order logic to propostional logic like Zap/Zapato. By the way: rather than lazy abstraction, Rustan called this strategy lemmas on demand, which I think is a good name.

If you're into this sort of thing, don't forget to submit a paper to this year's CAV workshop on Software Model Checking (SoftMC)! The deadline is May 19th.

- March 2005 -

I have been to many research meetings, workshops, conferences, etc in my life. But nothing compares to the meeting I just finished up. I spent the weekend in Paris working with Andreas Podelski and Andrey Rybalchenko. We did not have access to a real office, so we worked in the Paris outdoor cafes. This is simply the best way of doing research ever. We went through countless pieces of paper as we scribbled notes about how to do termination proofs. We went through countless coffees, and mineral waters. Without email or interruption we got a lot of work done --- and pretty bad sunburns too ;-). As he used to live in Paris, Andreas also appears to know a lot of great restaurants and fabulous people.

My colleague here at the Cambridge lab, Georges Gonthier, has done something really amazing: he has formalized and completely proved the four-colour theorem using the Coq mechanical theorem prover. There's a nice article about it in the March 4 edition of Science called What in the Name of Euclid is Going on Here?. Another nice article about the proof appeared in the Economist magazine on March 31st called Proof and beauty. Another brief article appeared on the register.

Two articles that I co-authored were accepted for publication at CAV:

Predicate Abstraction via Symbolic Decision Procedures
Shuvendu Lahiri, Thomas Ball and Byron Cook
CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)
Cogent: Accurate theorem proving for program verification
Byron Cook, Daniel Kroening, Natasha Sharygina
CAV'05 tool paper [International Conference on Computer-Aided Verification] (Edinburgh)

I'll make electronic copies available when we have the final versions done. An extended version of the paper on Cogent is available as an ETH technical report number 473.

Josh Berdine and Joel Ouaknine both visited me here at my lab. They gave great talks. Josh Berdine spoke about an automatic tool for proving separation logic conditions. Joel Ouaknine spoke about ASAP, which speeds up decision procedures for Presburger arithmetic (described in a CAV paper).

- February 2005 -

I'm in Seattle now for a while.

- January 2005 -

Moshe Vardi and Anuj Dawar are organizing a very impressive array of workshops here in Cambridge at the Isaac Newton Institute for Mathematical Sciences.

In February I'll be visiting Tom Melham and Joel Ouaknine at the Oxford computing laboratory and will be giving a department seminar. Then I'm off to Sweden to visit Mary Sheeran and Koen Claessen at Chalmers. Then I head off to Seattle for Microsoft Research's annual internal company-wide demonstration of new technology called TechFest. Then I'm off to Paris where I'll speak at ASM 2005.

- December 2004 -

I took some time off this month to spend christmas through new year's day with my family. Essentially we spent much of our time cooking and listening to the BBC radio. My son (and I) learned how to make flash animations. Here are some examples. Note: be sure to turn your sound on. We also went to several choral performances, including one by a university "nation" group from Uppsala, Sweden.

I be an invited speaker at this summer's Workshop on Empirically Successful Classical Automated Reasoning and Workshop on Disproving at CADE.

- November 2004 -

I'm going back to Zurich to give a colloquium talk at ETH.

Stella and Al came to Cambridge to celebrate Thanksgiving.

I moved from the north side of my lab to the south side. From my window I can see the construction site of the new Centre for Advanced Photonics and Electronics. I'm enjoying this view: my window is thick, so I can't hear a thing.....and it looks like an enormous lego project. Here's a live picture. In fact: from the live picture you can see building on the left and but my office window is just out of range.

- October 2004 -

Scott Stoller, Willem Visser and I are organizing another Workshop on Software Model Checking (SoftMC '05).....this time in Edinburgh. This workshop be held the day after CAV ends.

Last week I visited Andreas Podelski and Andrey Rybalchenko at the Max-Planck-Institut für Informatik in Saarbrücken. I also visited Daniel Kroening at Eidgenössische Technische Hochschule (ETH) in Zürich.

- September 2004 -

I spent 3 days back in Seattle this month, where I met with a number of teams who are building various types of symbolic program analysis engines. I also spoke at this workshop in Utah.

- August 2004 -

Daniel Kroening is coming to visit me at the lab here at the end of this month.

Don Syme helped me port Zapato from O'Caml to a soon to be released version of F#. F# is simply amazing. I couldn't believe it when Zapato (with just a few tweaks) compiled in F# and ran with no problems. Then Don started doing his magic with various .net profiling tools, suggesting small modifications that wildly improved the performance of the prover's F# compiled binary. Sometimes really great software makes me happy. Now I want to port all of SLAM.

While on the subject of commercial uses of functional programming languages, John Launchbury first hit me up to help him co-organize a workshop for commercial users of functional programming, and then asked me to give a talk too. So it looks like I'll be in Utah in late September. This workshop is the day before ICFP.

Last week I was in Palo Alto, CA where I gave a talk at the summer school on the combination of decision procedures. At the end of the last day some of us took a walk at Russian Ridge.

Before that I had a nice visit to Microsoft in Redmond, and the Seattle area. I attended a Bill Gates review of work by Shaz Qadeer, Jakob Rehof, Sriram Rajamani and the others in the SPT research group at MSR-Redmond. I also met with a number of my other collegues about research and development activities.

- July 2004 -

Moved to Cambridge this month.

- May 2004 -

Getting ready to move to Cambridge.

- March and April 2004 -

Here's a bit of information from the Windows division on Static Driver Verifier.

The short paper on the Zapato theorem prover that we submitted to CAV was accepted for publication:

Zapato: Automatic theorem proving for predicate abstraction refinement
Thomas Ball, Byron Cook, Shuvendu K. Lahiri, and Lintao Zhang
CAV'04[Computer Aided Verification] (Boston)

I've been traveling a great deal recently. I went to Barcelona, where I attended TACAS and other ETAPS conferences. I then gave talks at Evergreen and OGI. These two talks were fun because I was able to see many old friends. Aside from the OGI-based attendees, many of my Oregon-based friends at Intel SCL, Galois and Synopsys were also able to come.

I then travelled to the Washington DC / Baltimore area and gave a research talk at an NSA-sponsored conference. There was a mixup at the rental car agency and I ended up with a very large Gran Marquis instead of the standard midsize car that I would usually rent:

Driving this car around DC and Maryland made me feel like a real DC area government type. I got a lot of respect out on the road. Like I was an FBI agent, or something. It was huge! You should have seen me trying to parallel park this thing in Georgetown.

While visiting the NSA I also visited their National Cryptologic Museum. I wasn't expecting much, but I was honestly amazed by this place. I spent 4 hours there. They have Cray and Thinking Machines computers. They have several Enigmas. They even have one that you can try. It was great.

Next stop: I'm about to leave for the Beyond Safety meeting that Andreas Podelski has kindly invited me to.

- February 2004 -

News: I have decided to move to Cambridge, UK after I complete my last remaining tasks on the first public version of SLAM/SDV. This should be sometime late in the summer. I'm joining Microsoft's Cambridge research lab where I will continue my line of research: theorem proving, model checking, programming languages.

By the way: Be sure to look at these new photographs that James has recently made.

- January 2004 -

Happy new year. Tommorow I'm leaving for France where I'll give a talk at INRIA and visit with Xavier Leroy. I'm also going to visit MSR-Cambridge and hang out with Don Syme.

- November and December 2003 -

November and December have been quite interesting. I've spent a little bit of time traveling. For example: I attended a research symposium in honor of Dick Kieburtz's retirement down in Portland, OR.

I also visited Lintao Zhang and entourage at Microsoft's Silicon Valley Research Lab for about 3 days. While in the bay area I saw many friends during the evenings, such as Satnam Singh, Marcus Tallhamn, and Arne Boralv. I learned a lot of Silicon Valley formal verification gossip. Oh. The big surprise was that I was able to see Niklas Een too. He's spent 3 months working at Jasper Design Automation on SAT-based FV strategies. I was able to catch him just before he returned to Sweden.

I've learned that a paper that I co-authored was accepted for publication at TACAS:

Refining approximations in software predicate abstraction
Thomas Ball, Byron Cook, Satyaki Das, and Sriram K. Rajamani
TACAS'04 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems] (Barcelona)

So I guess that I'll see you in Barcelona if you're attending.

Happy holidays.

- October 2003 -

The Windows Driver Developer Conference was a big success. Our team worked hard on a version of SDV/SLAM for this conference. I've also been working on several research papers.

Henrik Persson (my friend from Prover) has now quit Prover and joined Microsoft in Sweden! During his first week they sent him here to Washington state for a conference on computer security. We went out for sushi and beer one night, and he came over to my house on another night.

I put up a small web page at Microsoft Research. And while I'm discussing trivial things, I'll also mention that I recently bought new glasses. I'll post a picture the next time someone takes a photograph of me with them on. They're very black, square, and chunky.

- September 2003 -

This month has been busy. We're working on the final details of our next release of static driver verifier. The various worms and viruses aimed at Microsoft have also made my life quite interesting.

I visited Ganesh Gopalakrishnan and his colleagues (of which there are too many to name in a list) at the University of Utah. I had lots of fun at the University. The Salt Lake City drinking scene leaves something to be desired, as I learned when I went out drinking with John Regehr. I had a pho dinner with (Jason) Yeu Yang and Konrad Slind. My friends here in Seattle find it somewhat silly that I choose to eat pho in Salt Lake City since I live within walking distance from hundreds of Pho restaurants in Seattle. Oh, and the Red Iguana was great!

Hey, do you want to see an image of me from high school? I'm the person not wielding the knife. The other person was my best friend. Unfortunately, he died several years ago.

- August 2003 -

I've just returned from the Portland Zine Symposium. Bee is a 'zine person who seems to know everyone in that world. We saw lots of old friends.

By the way: I've now been at Microsoft for a year. It seems like I've only been here for a couple of weeks. When I was at CAV, one of the most popular questions was "How is it at Microsoft?" My answer: "Things could not be better. I'm having the time of my life!"

For those of you non-Microsoft employees who want to try using Static Driver Verifier and SLAM, you should come to the Windows Driver Developer Conference.

- July 2003 -

I spent 2 weeks of this month in Boulder, CO. I spent the first week attending CAV/SoftMC. I spent the second week with my family.

CAV/SoftMC was good. I really enjoyed the session on theorem proving. The session consisted of two talks: one on Verifun (which is very relevant to my own work at Microsoft) and the second was by Shuvendu Lahiri. In addition to the sessions, I had ample time to speak with my friends, and I learned a lot of new formal verification ideas and techniques. This year's FV buzzword? Interpolants

My vacation time was great. When I was in high school I spent a lot of time hanging out at Mt. Falcon park. I went back during my visit and spent the afternoon.

- June 2003 -

Here's an interesting article that appeared in the the economist magazine about static analysis and model checking of software. It even mentions my project (static driver verifier, which is based on SLAM):

Building a better bug-trap

- May 2003 -

Static Driver Verifier has been creating some buzz within the Base OS group at Microsoft. I've given several well-recieved talks to VPs and will be giving a big talk soon to all of the Windows OS developers. We've now scoped out the next version of the tool (we plan to make the next release in November) and we're all ready making great strides! It looks great, works faster, works better, and we're finding amazing driver bugs. I'm having a lot of fun with a new theorem prover that I'm writing for pure C expressions (along the lines of Simplify, Verifun, CVC, etc).

I'm really excited about John Harrison's upcoming book on theorem proving. I've read a draft and its easily the best book technical book I've ever read. Its a book (with complete source code) on the different strategies for automating theorem proving. He's already made the code available, you should check it out!

- April 2003 -

A paper that I wrote with Shuvendu Lahiri, and Randy Bryant was accepted for publication at CAV. Its called A Symbolic Approach to Predicate Abstraction.

On a related note: Shuvendu Lahiri is going to intern with our team at Microsoft Research this summer!

We're making good progress at Microsoft on the SLAM software model checker. The other day our team released a tool based on SLAM to the Windows Base OS group. Its called Static Driver Verifier.

- March 2003 -

A paper I wrote with Gunnar Andersson, Per Bjesse and Ziyad Hanna was just accepted for publication in the IEEE Transactions on CAD. It's called Design Automation with Mixtures of Proof Strategies for Propositional Logic.

- January 2003 -

Scott Stoller, Willem Visser and I are organizing the second Workshop on Software Model Checking (SoftMC '03). We're holding the workshop just after CAV in Boulder, Colorado.

- November 2002 -

I was recently in Portland to attend FMCAD'02. I saw a lot of good talks. The best one? Hmmmm, I'd say Modeling and Verification of Out-of-order Microprocessors using UCLID by Lahiri, Seshia, and Bryant.

Per Bjesse tells me that he's joining Jim Kukula and crowd at Synopsys.

- August 2002 -

I'm now at Microsoft.

- May 2002 -

I've decided to leave Prover. Good luck Mary, Arne, Gunnar, Marcus, Per, and everyone else. It was a crazy time! Good-bye Crowsenburg's, good-bye to my office on Indie-rock-block, good-bye Portland.

What am I going to do with myself? Well. For the first time since I was 16, I'm going to take the summer off. In August I'll then join Tom Ball and Sriram Rajamani at Microsoft to work on the SLAM project.

Check out the art that James made while living in our basement last summer. Several of the pieces are now used on the new Delgados album: Hate.

- April 2002 -

Our DAC submission was accepted for publication:

A proof engine approach to solving combinational design automation problems
Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna
DAC'02 [Design Automation Conference]

Ok! I know: It has a hokey title. If you read it you'll notice that it also has a somewhat brain-dead premise. Sorry: its the only way we could get it past Prover's PR engine. The performance figures are really good though.