Model-checking and software

One of the most frequently asked questions from high school students interested in computing is on the difference between computer science and computer engineering. There are many similarities, of course, including the chance to solve world-changing problems, the dynamism and creativity of the field, and great job opportunities. But at the risk of over-simplifying, I usually say that CPE has relatively more emphasis on hardware and CS has relatively more emphasis on software. And then, tongue-in-cheek, I sometimes go on to make cheap shots like claiming that software is what really makes computing so flexible and powerful, and pointing out that there are way more companies that design and build software than there are that design and build microprocessors.

Of course I’m biased on the issue. But software just continues to amaze me at how challenging and interesting it is. For example, there is an interesting interview with the 2007 Turing Award winners, published in the July 2008 issue of CACM, on the topic of ‘model-checking.’ Model-checking is the modern descendant of (provable) program correctness; it has had some good successes and continues to receive attention from some really smart people. There is still much to do, however, especially on the software side. According to Joseph Sifakis, ‘For hardware, it’s relatively easy to extract mathematical models, and we’ve made a lot of progress. For software, the problem is quite a bit more difficult.’ Fellow award winner, Edmund Clarke simply says, ‘software verification is a Grand Challenge.’

Leave a Reply