Month: May 2012

  • Academic Bug-Finding Projects in the Long Run

    A number of computer science researchers, including me, have made careers out of creating tools that automate, at least partially, the process of finding bugs in computer programs. Recent work like this can be found in almost any good systemsy conference proceedings such as SOSP, OSDI, ASPLOS, ICSE, or PLDI. Examples go back many years,…

  • Damn You, Zork II

    Some significant part of my middle school years (age 11-14, roughly) was spent struggling with a couple of text adventure games and none of them was more tantalizing or frustrating than Zork II. In particular, the bank and baseball maze parts of this game completely stopped me, despite my large piles of notes and countless…

  • Recording a Class at Udacity

    A good chunk of my time between the end of Spring semester and now was spent recording a class on software testing at Udacity. This piece isn’t a coherent essay but rather some random impressions and thoughts. The main questions are: What is an online course supposed to look like? How can we keep students…

  • Why Isn’t C Memory Safe Yet?

    Memory safety errors in C/C++ code include null pointer dereferences, out-of-bounds array accesses, use after free, double free, etc. Taken together, these bugs are extremely costly since they are at the root of a substantial fraction of all security vulnerabilities. At the same time, lots of nice research has been done on memory safety solutions…

  • The Last Mile for a Verification Problem

    A few weeks ago my student Lu Zhao defended his PhD thesis and we were lucky to get his external committee member, Magnus Myreen, to attend in person since he was in the USA anyway for a meeting. While he was out here, Magnus gave a talk on some not-yet-published work that is really cool.…

  • When Will Software Verification Matter?

    When will average people start to use formally verified software? Let me be clear right from the start that I’m not talking about software that has been subjected to static analysis or about software that implements proved-correct algorithms, but rather about software whose functional correctness has been verified at the implementation level in a way…

  • Software Testing Using Function/Inverse Pairs

    One of the hardest problems in software testing is finding convenient, strong oracles—programs that can tell us whether the software under test worked correctly. Weak oracles, such as checking to make sure a program doesn’t crash, are always available, but not always of much use. An example of a strong oracle would be a reference…