Embedded in Academia

Category: Software Correctness

  • Operant Conditioning by Software Bugs

    Have you ever used a new program or system and found it to be obnoxiously buggy, but then after a while you didn’t notice the bugs anymore? If so, then congratulations: you have been trained by the computer to avoid some of its problems. For example, I used to have a laptop that would lock…

  • Software Testing Using Easy Cases

    Chapter 2 of Street Fighting Mathematics is called Easy Cases. The idea is very simple: A correct solution works in all cases, including the easy ones. Solution 2 in this writeup of the napkin ring problem is a fun example of applying this principle. Easy cases can be exploited for software testing as well as…

  • Oracles for Random Testing

    Random testing is a powerful way to find bugs in software systems. However, to actually find a bug it’s necessary to be able to automatically tell the difference between a correct and an incorrect execution of the system being tested. Sometimes this is easy: we’re just looking for crashes. On the other hand, there are…

  • How Does Formal Verification Affect Software Testing?

    This has been a difficult piece to write and I’ve already deleted everything and started over more than once. So, I’m going to take the easy way out and structure it as a sequence of questions and answers. What does formal verification mean? Something like “using mathematical techniques to convincingly argue that a piece of…

  • Writing Solid Code

    After 10 short years as a university-level CS instructor, I’ve finally figured out the course I was born to teach. It’s called “Writing Solid Code” and covers the following topics: Testing—There are lots of books on software testing but few that emphasize the thing I need students to learn, which is simply how to break…

  • How Did Software Get So Reliable Without Proof?

    Tony Hoare’s 1996 paper How Did Software Get So Reliable Without Proof? addresses the apparent paradox where software more or less works without having been either proved correct or tested on more than an infinitesimal fraction of its execution paths. Early in the paper we read: Dire warnings have been issued of the dangers of…

  • Certifying Compilers Using Random Testing

    Before a tool such as a compiler is used as a critical component in an important software project, we’d like to know that the tool is suitable for its intended use. This is particularly important for embedded systems where the compiler is unlikely to be as thoroughly tested as a desktop compiler and where the…

  • The Hidden Cost of Compiler Bugs

    I have a hypothesis that compiler bugs impose a noticeable but hard-to-measure tax on software development. I’m not talking so much about compiler crashes, although they are annoying, but more about cases where an optimization or code generation bug causes a program to incorrectly segfault or generate a wrong result. Generally, when looking at a test case…

  • Cyber War

    I recently read Richard Clarke’s Cyber War. Although I didn’t learn anything new on the technical side, that isn’t the focus of the book. Clarke’s main agenda is to build awareness of the uniquely vulnerable position that the United States finds itself in as well as proposing national policies that might lead to a more…

  • It’s Time to Get Serious About Exploiting Undefined Behavior

    [Note: I promise, this is almost my last post about undefined behavior for a while. Maybe just one more in the queue.] The current crop of C and C++ compilers will exploit undefined behaviors to generate efficient code (lots of examples here and here), but not consistently or well. It’s time for us to take this…