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.
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#."
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.
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.
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.
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. ;-)
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.
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)
My new dutch bike!
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)
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.
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.
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
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.
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.
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.
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.
Microsoft's research division has put up an article about TERMINATOR on their website.
- 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)
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) .
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:
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)
- Terminator: Beyond Safety (short tool description)
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
CAV'06 [International Conference on Computer-Aided Verification] (Seattle)
- 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)
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.
- Alex Aiken
- Alessandro Cimatti
- Edmund Clarke
- Carla Gomes
- Aarti Gupta
- Orna Grumberg
- Daniel Kroening
- Shuvendu Lahiri
- Sharad Malik
- Ken McMillan
- Robert Nieuwenhuis
- Ofer Strichman
- Termination Proofs for Systems Code
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)
- 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)
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!
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)
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.
Check out Smallfoot, which comes from The East London Massive.
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.
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.
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.
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.
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.
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.
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.
- 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.
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.
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)
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).
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.
I be an invited speaker at this summer's Workshop on Empirically Successful Classical Automated Reasoning and Workshop on Disproving at CADE.
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.
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.
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.
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.
By the way: Be sure to look at these new photographs that James has recently made.
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.
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.
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.
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.
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.
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!
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.
Per Bjesse tells me that he's joining Jim Kukula and crowd at Synopsys.
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.
- 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.