Verifying absence of integer overflow

June 7, 2010 2 comments

One class of errors we need to guard against when writing critical software is arithmetic overflow. Before I go into detail, I invite you to consider the following program and decide what it prints:

#include <stdio.h>
int main(int argc, char *argv[]) {
unsigned int x = 42;
long y = -10;
printf("%s\n", (x > y ? "Hello, normal world!" : "Hello, strange world!"));
return 0;

Read more…

Specification with Ghost Functions

May 26, 2010 Comments off

In my previous post I showed that the C expression sublanguage extended with quantified expressions (forall and exists) is insufficient to allow some specifications to be expressed. I presented this function (annotated with an incomplete specification) to average an array of data:

int16_t average(const int16_t * array readings, size_t numReadings)
pre(readings.lwb == 0; readings.lim == numReadings)
pre(numReadings != 0)
post(result == ? /* sum of elements of readings */ /numReadings)
int sum = 0;
size_t i;
for (i = 0; i < numReadings; ++i)
keep(i <= numReadings)
keep(sum == ? /* sum of first i elements of readings */ )
decrease(numReadings - i)
sum += readings[i];
return (int16_t)(sum/numReadings);

Read more…

Expressing the Inexpressible

May 24, 2010 3 comments

When writing preconditions, postconditions and other specifications for C programs, sometimes we need to write expressions that can’t be expressed in plain C. That’s why formal verification systems based on annotated programming languages almost always augment the expression sublanguage with forall and exists expressions. In previous posts, I’ve introduced ArC’s implementations of these. For example, the following expression yields true if all elements of the array arr are between 0 and 100 inclusive:

forall ind in arr.indices :- arr[ind] >= 0 && arr[ind] <= 100

Here, ind is declared as a bound variable that ranges over the values in the expression that follows the keyword in, which in this case is all the indices into arr. Read more…

Verifying a binary search, part 2

May 6, 2010 2 comments

In my last entry I showed how to use a correct-by-construction approach to develop a binary search function. We got as far as specifying the function and the loop, but we left the loop body undefined. The function declaration looked like this: Read more…

Verifying a binary search

May 5, 2010 Comments off

In the last post, I covered some different levels of formal verification that you may be interested in, and showed how to add minimum annotation to the linearization example to allow ArC to prove predictable execution. The example provided a prototype for the binary search function it called, to which we added a minimal postcondition, so that it looked like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
 post(result <= nElems);

Read more…

What are you trying to prove?

April 27, 2010 9 comments

If you’re thinking of using formal verification to increase the quality and reliability of your software, one of the first decisions you need to make is what you want to prove. Roughly speaking, you have three levels to choose from: Read more…

Danger – unsigned types used here!

April 7, 2010 21 comments

By way of a change from the last two posts on formal verification, this time I’m going to talk about using unsigned types in C/C++. Modern programming languages such as C# and Java don’t provide unsigned types, with good reason (actually, C# does have unsigned types, but only for the purpose of interfacing to COM objects written in other languages, and they are not used in the .NET Framework API).

To illustrate the dangers of using unsigned types, I invite you to consider this example Read more…

Verifying loops: proving termination

March 31, 2010 6 comments

If you’ve stuck with me so far in this mini-series on verifying loops, give yourself a pat on the back  before reading further. When it comes to formal verification of single-threaded software, loops are the most challenging constructs to verify. Read more…

Verifying loops – part 2

March 29, 2010 2 comments

Last time I showed how it was possible to analyse a loop-free and recursion-free program or function to determine its semantics (i.e. its weakest precondition and its postcondition), but that this didn’t work when we have loops. To make it possible to analyze loops thoroughly, Read more…

Verifying loops in C and C++ (intro)

March 22, 2010 1 comment

When it comes to formal verification of single-threaded programs, one of the hardest constructs to verify is the humble loop. If a function contains no loops and no function calls, then a static analyser can trace through the function, looking for constructs (such as indexing an array, or dividing one number by another) that have an implied precondition Read more…