Ensuring full functional correctness of computer programs has long been a holy grail for computer scientists. To prove without a doubt that a computer program does only what it is intended to do, and nothing else, is an exhilirating concept. One natural question is wether or not these types of guarantees really are required of computer software; after all, our desktop computers frequently behave in ways we do not want them to, yet we persevere. The problem is that only a fraction of the computers we find in modern society sit on our desktops. The vast majority of computers are small embedded devices that can be found in cars, in airplanes, in medical equipment or in MP3-players. Whereas we readily accept that our laptop behaves unpredictably, we want to have certain guarantees regarding the software that operates the air-bag in the cars we drive, or administers medicine at hospitals.
Famous software bugs
One of the most famous software bugs in history is the one that caused the destruction of the Ariane 5 rocket on June 4:th 1996. Roughly 40 seconds after launch, the rocket suddenly changed direction causing the self destruct mechanism to kick in. Later inquiries revaled that the bug was caused when the program tried to store a too large number in a signed 16-bit integer field (the highest possible value is 32767), causing a run-time error. The rocket and its cargo was valued at roughly 500 million US dollars.
Another famous bug was the one that caused the loss of Nasa's Mars Climate Orbiter in 1999. The bug originated from the fact that different engineering teams used different units of measurement -- one using the metric system, and the other the imperial units of measuerment. This caused the orbiter to miscalculate its entry into Mars' orbit and it is believed that it burned up in the atmosphere. The orbiter was valued at roughly 125 million US dollars.
State of the art
Even though there is a clear need to ensure that software functions the way it should, the dream of shipping fully verified programs has proven very difficult to realise. The main reason for this is that the techniques available today require a PhD in computer science or mathematics to use. Also, they do not scale well to anything above simple toy examples. Programs of the complexity used in industry are simply out of scope for the time being. There are, however, two notable achievements in the area of software verification. The first one is the verified L4 micro-kernel done at Nicta, and the second is the CompCert project that verified a small optimising C-compiler. Both these projects verify programs that span roughly 7500 lines of code, and the formalisation effort required was several man decades. These projects represent the state of the art, but they also indicate that we have a long way to go before these techniques can be used in practice
My research
I am currently the head of a project that aims to create a general-purpose framework for software verification. This project has two parts. The first is to create a framework where researchers can efficiently prototype new programming languages and provide an environment in the interactive proof assistant Coq where programs written in these languages can be verified. The second is to use this framework to create an Eclipse plugin that allows devlopers to verify Java programs using the standard Eclipse Java perspective. One of our main design goals is to create a tool that can be used by programmers who know a bit of mathematics, and not only by mathematicians who know a bit of programming. The long term goal is to create a tool in which we can write a program, its specification, and finally prove the program correct with respects to its specification, all in one tool.
Parallel to the tool-development, we are proving the correctness of various modules of the C5 Generic Collection Library such as snapshottable trees or linked lists with views. Both of these use techniques, such as pointer aliasing, that are typically difficult for verification tools to reason about.