Category: Software Correctness

  • Draft Paper about Integer Overflow

    Last Spring I had a lucky conversation. I was chatting with Vikram Adve, while visiting the University of Illinois, and we realized that we working on very similar projects — figuring out what to do about integer overflow bugs in C and C++ programs. Additionally, Vikram’s student Will and my student Peng had independently created…

  • Overflows in SafeInt

    Update from Friday 9/23: The SafeInt developers have already uploaded a new version that fixes the problems described in this post. Nice! I have a minor obsession with undefined behaviors in C and C++. Lately I was tracking down some integer overflows in Firefox — of which there are quite a few — and some…

  • Better Random Testing by Leaving Features Out

    [I wrote this post, but it describes joint work, principally with Alex Groce at Oregon State.] This piece is about a research result that I think is genuinely surprising — a rare thing. The motivating problem is the difficulty of tuning a fuzz tester, or random test case generator. People like to talk trash about…

  • Fuzzing Linux Kernel Modules?

    I’ve been thinking about what would be the best way to fuzz-test a Linux kernel module, for example a filesystem. Of course this can be done in the context of a live kernel, but for a variety of reasons I’d prefer to run the LKM in user space. At the source level, the interface to…

  • Testing Commercial Compilers

    A few weeks ago a reader left this comment: Just out of curiosity John, have you approached any of the big commercial compiler companies about getting free licenses for their products? I don’t work in the compiler business but if a university research time offered to rigorously test my software, for free, I’d say yes.…

  • Isolation with a Very Small TCB

    A basic service provided by most computer systems is isolation between different computations. Given reliable isolation we can safely run programs downloaded from the web, host competing companies’ sites on the same physical server, and perhaps even run your car’s navigation or entertainment software on the same processor that is used to control important system…

  • Proposal for Automated Compiler Bug Reports

    [Yesterday I submitted a proposal to Google for a modest amount of money to work on turning large random programs that expose compiler flaws into concise bug reports. Below is a transcription that is mostly faithful (citations are omitted and I changed the example bug report from a floating figure into inline text). Feedback is…

  • ISSTA 2011

    Earlier this week I gave one of the keynote talks at ISSTA, the International Symposium on Software Testing and Analysis. A year ago Matt Dwyer, the general chair, sent me the following invitation: I would like to invite you to give a keynote talk to the meeting about the challenges in testing, dynamic and static…

  • Split Vote

    In my group’s recent compiler testing paper we wrote: We have never seen an “interesting” split vote where randomized differential testing of a collection of C compilers fails to produce a clear consensus answer Randomized differential testing is just a fancy way of describing this process: Randomly generate a test input Run it through several…

  • Why Verify Software?

    People like me who work on software verification (I’m using the term broadly to encompass static analysis, model checking, and traditional formal verification, among others) like to give talks where we show pictures of exploding rockets, stalled vehicles, inoperable robots, and crashed medical devices. We imply that our work is helping, or at least could…