Teen pregnancy a good thing?

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!
at

En route to San Francisco/Colorado/CMU

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

text-only web browsing!

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

Trends in concurrency summer school

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

Marktoberdorf summer school

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

SLAM/SDV rule kit now available!

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
at

Ranking abstractions

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

Postdocs, interns, apply now

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

Shape analysis, for real!

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

Sad days.....

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

Comings and goings.....

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
at

Old blog (April '02 through Nov '07)

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

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:

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

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:

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

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:

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


- 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 ;-)

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:

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


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

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:

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

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:

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):


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

at
Subscribe to: Posts (Atom)