Month: January 2011

  • Who Verifies the Verifiers?

    Verification tools, like all complex software systems, contain design flaws and implementation errors. Moreover, they are not necessarily very easy to test. The other day I started to address the question: If someone claims that a piece of software has been formally verified, what should you believe about the software? The previous piece was non-technical;…

  • The Piano Test for Program Verification

    [Update from Feb 1 2011: I’ve written a new post that adds some technical details.] Here’s a little thought experiment: You’re spending the day visiting the Utah computer science department. We’re chatting and I describe a software verification project where my group has proved that some particular version of OpenSSH is memory safe: it will…

  • Elk and Winter Light

    [nggallery id=31]

  • Good Book: Idaho Falls

    This book, like the one I wrote about yesterday, is a horror story for engineers. Idaho Falls is about the SL-1, a prototype nuclear reactor in the desert in Idaho. Although it had been designed for a 3 MW thermal capacity, in early 1961 its output briefly reached something like 18 GW when the single…

  • Good Book: Space Systems Failures

    Space Systems Failures is like a horror novel for engineers: years of people’s lives and hundreds of millions of dollars are wasted because somebody crossed a wire or skipped a test. The real reasons for failures of launch vehicles and their payloads, however, are more interesting: Margins are slim because adding margin is expensive System…

  • The Synergy Between Delta Debugging and Compiler Optimization

    Before reporting a compiler bug, it’s best to reduce the size of the failure-inducing input. For example, this morning I reported an LLVM bug where the compiler enters an infinite loop when compiling this C code: static int foo (int si1, int si2) { return si1 – si2; } void bar (void) { unsigned char…

  • The 5+5 Commandments of a Ph.D.

    [This post is co-authored and co-posted with my colleagues Matt and Suresh. Comments should all go to Suresh’s version.] There have been a lot of Ph.D.-bashing articles lately. There have been some spirited defenses of a Ph.D. too. Most of these articles make good observations, but they’re often about the larger Ph.D. ecosystem and therefore…

  • Gear for Getting Outside in Winter

    Since I’m not a big skier, I didn’t get out a lot in winter during my first few years in Utah. When springtime came, I would just tough it out and get into shape the hard way — go on a few long hikes and suffer appropriately. This worked because I was in my 20s.…

  • The Future of Software System Correctness

    A few weeks ago I re-read Tanenbaum et al.’s 2006 article Can We Make Operating Systems Reliable and Secure. They begin by observing that it would be nice if our general-purpose operating systems were as reliable as our cars and televisions. Unfortunately, Tanenbaum’s vision is being realized in the worst way: as the amount of…

  • Almost Everything in Subversion

    Every file I use on a day to day basis — excluding only data shared with other people, email folders, and bulk media — is kept in a big subversion repository. For the five years that I’ve been doing this, I’ve averaged 3.5 commits per day. Overall it works really well. Advantages of this scheme…