A benchmark for C program verification

TL;DR

This paper introduces a benchmark comprising twenty-five C programs designed to evaluate and compare the effectiveness of formal verification tools, facilitating system demonstration, effort comparison, and competitive evaluation.

Contribution

It provides a standardized benchmark with a scoring formula for assessing C program verification systems, promoting fair comparison and progress in the field.

Findings

Benchmark enables systematic evaluation of verification tools.

Scoring formula allows quantifiable comparison.

Facilitates demonstration and competition in C verification.

Abstract

We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.

Figures

Equations

$$25\times\mbox{$4$ points}=\mbox{$100$ points}$$

Full text

1 Introduction

Here is a challenge for people who are interested in practical C program verification using formal methods. Show us how to verify the correctness of the twenty-five programs in this paper. The sources of these programs can be found at:

[TABLE]

If you take this challenge, we will add your work (or a pointer to it, as you prefer) to the repository.

In our Sovereign project [8], which has as its focus the safety and correctness of industrial programs, we are interested in practical C program verification. Therefore we would like to have a clearer overview of frameworks for doing this. At first we planned to only have a few small programs for trying out the different systems (e.g., [1], [6], [7], [11], [15]). However, this then grew into this benchmark.

The original idea of this benchmark was that it should be about five programs. It will be completely clear what these programs are when one sees the names:

[TABLE]

The few keywords given here indicate why we chose these five programs. (Obvious additions to this list are fib and gcd, but we consider these ‘more of the same’ with respect to fac.)

For each of these programs we now have several variants, ranging from very small with only a few lines of code to significant programs with reasonable behaviors. We intentionally kept the programs in this benchmark on the spectrum:

simplest version**real life implementation

Altogether this gives twenty-five variations on those five programs. Three of these are not written by us, but are GNU implementations [20] that are actually used by many people.

To turn this into a benchmark, then, we award four points for a proper verification of any of the programs. This means that it is possible to score:

[TABLE]

To get all four points for a program, one should both show that it does not exhibit undefined behavior and prove its functional correctness. Points will be subtracted for the following simplifications:

[TABLE]

For example, if one only verifies functional correctness of a model of the program, one only gets $4-1-2=1$ point ($-1$ for not verifying well-definedness, and $-2$ for only verifying a model) instead of four. We include the option to modify the code a bit (with the loss of one point), because we expect some frameworks to have restrictions on the code they can verify.

To phrase this more positively, another way to state the way points are awarded is:

[TABLE]

For the last point it is allowed to add special comments to the code to enable the verification, like in the ACSL language [2].

What it means to correctly verify defined behavior, whether a tool models C accurately (a subject that can lead to heated debate), and how much modification to the code is allowed for the program to still be ‘the same’, we intentionally leave open. This is a friendly challenge, and should not be taken too seriously: if someone wants to award him- or herself a certain number of points for a verification effort, they should feel free to do so. We primarily hope this ‘benchmark’ will be useful for demonstrating and comparing verification frameworks on actual C code.

Exactly what it means to ‘verify’ code like this we also intentionally leave open. One is free to decide for oneselves what the specification for the programs should be. In practice, we expect that this means that one has to give:

• •

Restrictions on the C implementation.

• •

Pre-conditions for the code, e.g., restrictions on the input.

• •

Specification of the behavior of the code, e.g., appropriate post-conditions.

The C standard [14] has the notion of implementation-defined behavior. This first item is about making explicit under what implementations the program should work.

For example, the last programs in our benchmark presuppose IEEE 754-compliant floating point numbers. While the object representation of floating point numbers is not implementation-defined (but unspecified), there is the STDC_IEC_559 pre-defined constant, which is implementation-defined. The restriction on the C implementation for these programs then might be that te implementation has to define that constant appropriately, in which case we can assume that the object representation for floating point numbers matches the IEEE 754 standard. Similarly, there might be restrictions on the integer sizes to be ‘large enough’, or struct layouts to be appropriate to the program.

Here then is a list of our twenty-five programs, with a table of the C features that each of these programs exercises:

program number

filename

type

lines of code

function calls

standard library calls

other library calls

recursion

preprocessor: includes

preprocessor: defines

input/output

threads

exit

break/continue

switch

labels/goto

arrays/pointers

function pointers

structs

unions

defined types

typedefs

floating point

IEEE 754 floating point

1

fac1.c C 3

2

fac2.c C 3

3

fac3.c F 9

4

fac4.c F 5

$\times$

$\times$

5

fac5.c S 20

$\times$ $\times$

$\times$

$\times$

$\times$

6

fac6.c S 70

$\times$ $\times$

$\times$

$\times$ $\times$

$\times$

$\times$

$\times$

7

cat1.c C 2

$\times$

$\times$

8

cat2.c S 13

$\times$

$\times$

$\times$

$\times$

$\times$

9

cat3.c S 76

$\times$ $\times$ $\times$

$\times$

$\times$

$\times$ $\times$

$\times$

$\times$

10

coreutils/src/cat.c R ${\sim}800$

$\times$ $\times$ $\times$

$\times$ $\times$

$\times$

$\times$

$\times$ $\times$

$\times$

$\times$

$\times$

11

malloc1.c F 16

$\times$

$\times$

12

malloc2.c F 28

$\times$

$\times$

$\times$

13

malloc3.c F 26

$\times$

$\times$

$\times$

14

malloc4.c F 180

$\times$

$\times$ $\times$

$\times$ $\times$ $\times$

$\times$ $\times$

15

glibc/malloc/malloc.c R $\hskip 4.0pt{\sim}6000$

$\times$ $\times$ $\times$

$\times$ $\times$

$\times$ $\times$

$\times$ $\times$

$\times$ $\times$ $\times$

16

qsort1.c F 23

$\times$

$\times$

$\times$

17

qsort2.c F 50

$\times$

$\times$

$\times$

$\times$

18

qsort3.c F 50

$\times$

$\times$

$\times$

$\times$

$\times$

19

qsort4.c F 30

$\times$

$\times$

$\times$ $\times$

$\times$

$\times$ $\times$

20

qsort5.c S 83

$\times$ $\times$ $\times$ $\times$

$\times$ $\times$

$\times$ $\times$

$\times$

$\times$

$\times$

21

sqrt1.c F 14

$\times$

22

sqrt2.c F 12

$\times$

$\times$

$\times$ $\times$

23

sqrt3.c F 9

$\times$

$\times$ $\times$

24

sqrt4.c F 190

$\times$

$\times$

$\times$

$\times$ $\times$

$\times$ $\times$ $\times$ $\times$

$\times$ $\times$

25

glibc/soft-fp/sqrtsf2.c R ${\sim}500$

$\times$

$\times$

$\times$ $\times$

$\times$ $\times$

$\times$ $\times$ $\times$ $\times$

$\times$ $\times$

There are different types of granularity in this list, ranging from only a fragment of a few isolated lines of code (in which case for example a Hoare triple for that fragment might be proved) to a full multi-file development that spans multiple directories. The four types are indicated with the following letters:

[TABLE]

The numbers of lines for the GNU programs are only rough indications. There are many files (including many header files) involved in these programs, and we did not establish exactly which files are needed for these programs. (In the list we only list the primary source file, but the verification should include all other relevant source files.) Also, the exact line counts will be dependent on the version of the software. We do not want to restrict the version that should be used for this challenge, but while developing this benchmark we looked at version 8.27 of coreutils, and version 2.24.90 of glibc:

[TABLE]

The listings in this paper only show the relevant parts of the programs. These are the parts that should be verified. However, in case it is useful to take other parts of these programs into account, that is of course allowed. Each of these programs (apart from two of the three GNU ones) is a program that can be compiled on its own, so each program has a main function in its file too.

2 Factorial

2.1 A simple for loop

The very first program fragment is a for loop, multiplying the numbers from 1 to n:

This program has a straight-forward counterpart in most programming languages, so it should be easy to model it in any system. The declarations of f, i and n are not part of this fragment, but of course should be taken into account when verifying this.

In practice, this program will exhibit integer overflow when n is too large. With 32-bit integers this happens for $\texttt{n}\geq 13$. The exact way this is specified in the pre-condition is left open. For example both ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{n}}}}}}<13$ and ${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{n}}}}}}!\leq\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{INT\textunderscore MAX}}}}}}$ might be reasonable choices for this.

2.2 Turing’s program

The second program fragment is very similar to the previous one, but is a bit more involved. This is a C rendering of a program by Alan Turing from his 1949 paper [21] on program verification:

This calculates factorial without using multiplication. The original version of this program was written for the Manchester Mark 1 computer [22], but as far as we know no C compiler for that computer exists.

2.3 A function

We now wrap the code in a function. This time the verification has to be about pre- and post-conditions of C functions, not of isolated statements:

We used more ‘C-like’ idiom in this example. For example, the update of the counter and the multiplication now happen together in a single statement, making this example slightly less trivial.

2.4 Recursion

We claimed that the for loop has a counterpart in most programming languages, but this might not hold for functional languages. Here is the obvious recursive definition of the factorial function in C:

When called with too large an n this program can overflow its stack (for example when compiled with gcc -O0 and called with 1000000 this happens). The C standard does not address that issue, but the verification of this code might take this into account in its pre-condition.

2.5 Big numbers

Until now the output of the code is meaningless for most inputs because of overflow. The program might as well just index in a small array to get the appropriate output. Here is a version of the program that uses the GMP library [10] to compute factorial for larger inputs:

A specification of this program should also contain appropriate specifications for the GMP types and functions being used here. This program computes the factorial of one million (a number of 5,565,709 decimal digits) in a few minutes.

2.6 Big numbers without a library

Here is a simple implementation of factorial with big number arithmetic without using an external library:

The output of the digits does not use printf, but prints the digits individually using putchar. However, for the error handling fprintf is used.

This program is about ten times slower than the GMP version.

3 Cat

3.1 The simplest input/output program

Input/output is underrated in C verification. For example, in the CH2O semantics from Robbert Krebbers’ very thorough PhD thesis [17] this is not properly modelled. However, we think that input/output (the way that software interacts with its environment) is a fundamental property of a program and should be treated as such.

The simplest program with both input and output just copies its input to its output. In Unix this program is called cat, and the simplest C implementation of this behavior is:

How the functional behavior of this program should be specified is not addressed in this paper.

3.2 Buffering

In practice the previous program is slow, even though getchar internally uses a buffer. By putting an explicit buffer in the program, it gets as fast as the GNU implementation of cat:

This program uses the size_t type, because that is what the fread function returns and the fwrite function expects. Therefore the verification framework should know about this type, in order to be able to verify this example.

This code is similar to the example program from [12].

3.3 A simplified version of the real program

Here is a simplified version of the GNU implementation of cat. The main missing functionality is that there are no command line options (‘flags’). Also, we simplified the code quite a bit:

This code does not use the standard C library functions fread and fwrite, but instead uses the basic Unix system calls read and write. Therefore, the code includes the unistd.h header file, and should be verified with a respect to a specification of a Unix environment.

3.4 The GNU version

This is the real program that the previous program was a simplified version of. When on a Linux system one runs cat, this is the code that is executed.

The file coreutils-8.27/src/cat.c contains 768 lines of code, but that code includes eight GNU header files, links to a function for handling command line options, and uses the GNU function xmalloc, a wrapper around the C standard library function malloc which is defined in a different file.

4 Allocate memory

4.1 The simplest allocator

Here is the simplest memory allocator for C possible. It just cuts off pieces of memory and does not support free:

This code does not satisfy the alignment restrictions on the real C malloc. All that is guaranteed is that a block with the appropriate number of bytes is returned.

This code is very similar to the memory allocator verified in [3, 4].

4.2 A typed allocator

If one does not need arrays, a memory allocator for C is simple to write. Here is an allocator that allocates objects of a given type T. (The definition of this type is intentionally not given in the code fragment shown, as it should be irrelevant for the verification.)

The code both has an array (to allocate from) and a linked list (for keeping track of the freed objects), which makes it a nice target for separation logic:

4.3 A typed allocator that does not need pointer casts

The previous program needs to get a pointer to a union cell from a pointer to the allocated T object that is in that cell. According to the C standard [14] this is allowed, as it says in 6.7.2.1/15:

[ …] A pointer to a union object, suitably converted, points to each of its members (or if a member is a bit-field, then to the unit in which it resides), and vice versa. [ …]

However, in some formal versions of the C semantics [18] this is not allowed. Therefore, here is a variant of this code where the user needs to keep track of the union cell for him- or herself, and that problem is not present:

4.4 A simplified version of the real program

Here is a very much simplified version of the GNU implementation of malloc and free in glibc:

Some features of the real GNU malloc that are missing from this version:

• •

no fastbins

• •

just a single regular bin

• •

no bitmap to quickly find non-empty bins (not needed, as there is just one bin)

• •

no sbrk to get more memory (just one static array)

• •

memory never returned to the system (the av_top pointer never decreases)

• •

no memory mapped blocks

• •

no thread-awareness

However, the free list in the one bin is still kept in sorted order, and still uses the fd_nextsize and bk_nextsize pointers to search for an appropriate block.

4.5 The GNU version

And again, the last program of this section is the full GNU implementation of malloc and free in glibc. The main file glibc/malloc/malloc.c in version 2.24.90 of glibc has 5,289 lines of code, but this file depends on many other files.

The file contains the sentence:

The implementation is in straight, hand-tuned ANSI C.

Exactly what it means to say that this code is ‘ANSI C’, and whether this is actually true, is an interesting question.

5 Quicksort

5.1 Straight-forward quicksort

Here is a very straight-forward version of a quicksort function for an array of doubles:

This function of course has to be called with quicksort(0, N - 1).

We tried to make this code as simple as possible. For example it contains no return or break and only has a single swap.

There is a variant of this in which there only is a single comparison between i and j (with the bounds in the recursive call different), but that really makes use of the fact that we used a[n] for the pivot. For that reason we decided not to take that variant here, even though it is still shorter. The version here also works with different choices for the pivot, like taking the median or mean of some elements in the array.

This program has the property that if the array is already sorted, then it needs stack space for the recursion proportional to the length of the array. On a Linux system with a (default) stacksize of 8MB, the full program, which has N equal to 666,666, fails after about three minutes with the error:

segmentation fault

It would be nice if the verification of this program would be compatible with this behavior, i.e., that it would not be possible to prove this program to be correct for too large N.

5.2 Hoare’s version of quicksort

Here is a variation on the previous program. This is a C rendering of the programs in the original publication on quicksort by Tony Hoare [13]:

This program uses goto instead of break. The original Algol 60 version of this code uses the call-by-name feature of Algol 60 (which is more like macro expansion), which is modeled here by giving the partition function pointers to the variables to be modified.

5.3 The algorithm in the real program

If we take the GNU implementation of quicksort, and simplify it and also make it only apply to arrays of doubles, this is what one gets:

This is just a variation on the previous programs, but it has a few nice features, like using a macro for swapping elements in the array. One probably wants to prove this macro correct, which means that just verifying the macro-expanded version of the program will not be too attractive in this case.

Apart from the fact that this function only sorts doubles instead of sorting arrays with elements of an arbitrary type, it omits two optimizations from the GNU version of this code. This uses insertion sort when the size of the subarray drops below a certain threshold, and it manages a (short) explicit stack for the recursive calls, instead of using the recursion of C.

5.4 Quicksort on arbitrary types

Here is a version of the simple version of quicksort that we gave in 5.1, but this time for arbitrary types, so this is an implementation of the interface of the qsort function in the C standard library:

Notable features of this program are function pointers, (void *) pointers, and the use of memcpy to copy C objects.

5.5 Parallel quicksort

Finally, here is a version of quicksort that uses threads. The basic idea of this program is that at most THREADS threads will be running. Once a recursive call gets a piece of the array of which the size is below THRESHOLD (which means the data will fit in the cache of one of the cores), a separate thread will be used for this if one is available. The count of free threads is kept in the variable available for which a mutex is used when updating it.

We did not use C11 threads for this, because we did not have a good implementation of it available. Instead this uses the pthreads library. The means the program might need to be compiled with -lpthread.

Again, algorithmically this is just the simple algorithm from 5.1:

6 Square root

6.1 Newton’s approximation

The last class of examples in this benchmark are implementations of the square root function on single precision floating point numbers. Here is a simple version of an implementation that uses the Newton method:

This will not always give exactly the right answer according to the IEEE 754 standard, but it will be close. If a float has finitely many different representations (which one might expect the C standard would enforce, because there are only finitely many different object representations), then this program will always terminate.

It is interesting exactly what is provable about this program in a C implementation where one does not know how the floating point implementation works in detail. Maybe if there are some guarantees about relative error bounds of the arithmetic operations, an error bound on the result of this function can be proved.

6.2 An approximation of square root by bit shifting

The IEEE 754 representation of floating point numbers allows for an approximation to the square root function that can be calculated extremely fast. The counterpart for the inverse square root function (both square root and inverse square root use exactly the same trick) is known as ‘the 0x5f3759df method’, after the magic constant that appears in it. (Comments in the first program that had this constant in it were evil floating point bit level hacking and what the fuck?)

The implementation just consists of considering the bits of the number by casting it to an integer, shifting those bits one place to the right, and then adding a magic constant to that integer representation:

It is surprising that this gives a sensible result. One is shifting one of the bits of the exponent into a bit of the mantissa, how is that going to make sense? However, when analyzing it more closely [5], it turns out that this does make sense, and that for sufficiently large inputs, it gives a continuous piecewise linear function that approximates the square root function quite well (it is exact on powers of four, see the graph in Fig. 1.) The maximum error occurs when the argument is twice a power of four, and the relative error on those values is $(1\frac{1}{2}-\sqrt{2})/\sqrt{2}=\frac{3}{4}\sqrt{2}-1\approx 6.0660\%\approx 2^{-4.0431}$, which means that generally the first three bits of the fractional part will be correct.

Unlike the code in the next section, this function also makes sense if floats do not have 32 bits single precision. All that is needed is that the bits are laid out in the style of a IEEE 754 representation. As was noted before, this can be established by the implementation-defined property of STDC_IEC_559 having an appropriate definition.

We had some discussion whether to include this program in our benchmark. We wanted our examples to be ‘realistic’, and this seems more of a cute hack than something resembling realistic code. Also, nowadays square root is supported by hardware, and getting a good approximation as a start for Newton’s method is not really important anymore. However, this program is about the bit representation of floating point numbers, and about using casts to reinterpret one type as another (which is a common thing in C). For this reason we decided to still include this as one of our examples.

6.3 An approximation of square root by bit shifting that does not violate effective types

The previous program uses type casts to get at the bits of a floating point number, in order to be able to shift them. However, that violates the effective type rules, as described in 6.5/7 of the C11 standard. In fact, when compiled using GCC with the -Wall and -O3 flags, the compiler emits the warning:

warning: dereferencing type-punned pointer will break strict-

aliasing rules [-Wstrict-aliasing]

We now give a version of the same program that uses a union to get at the bits of the float, which means it does not suffer from this problem:

Using a union to get at the bits of an object is allowed by the C11 standard, as in footnote 95 of 6.5.2.3/3 it reads:

If the member used to read the contents of a union object is not the same as the member last used to store a value in the object, the appropriate part of the object representation of the value is reinterpreted as an object representation in the new type as described in 6.2.6 (a process sometimes called “type punning”). This might be a trap representation.

When using unions, it is harder to write the constant to be added to the expression in a way that it will work whatever the number of bits in the floating point representation, and in such a way that the compiler will insert it as a constant in the code at compile time. To keep the program small, we therefore expanded this constant to its value for 32-bit floating point numbers: 0x1fc00000. This means that to work correctly, this program needs an implementation with 32-bit IEEE 754 floats.

6.4 A simplified version of a serious implementation

The GNU library glibc contains software implementations of the IEEE 754 operations in the subdirectory soft-fp. In the case of square root, the algorithm used is the square root analog of long division. The GNU code for this consists of a whole stack of macro definitions. When expanding all these definitions, and simplifying everything quite a bit, one gets:

This code implements IEEE 754 behavior, but (as the primary simplification) only implements the default rounding mode. The full GNU version supports the other rounding modes as well. Also, the full version implements more possible variant behaviors on not-a-numbers.

Most of this code is about getting at the bits at the start and reassembling the floating point number at the end, and about handling various special cases like infinities, not-a-numbers, and denormalized numbers. The actual algorithm for the ‘long division’ analog is in lines 103–125.

6.5 The GNU version

And the last program in our verification benchmark is the actual implementation of square root in libc/soft-fp. That code is a bit obfuscated, because many of the macros implement the operations for different floating point sizes at the same time. The function that should be verified is __sqrtsf2, implemented in the file sqrtsf2.c:

Of course the macros defined through the #include lines pull in lots of other code from other files, and expand this program significantly.

In the latest versions of glibc the source code of square root in libc/soft-sp has been moved to a larger file that contains many arithmetical operations together. However, we prefer to have the 25th program in our benchmark be about a single small source file that we essentially can include in this paper. For this reason, this benchmark stays linked to version 2.24.90 of glibc.

7 Versions

The benchmark presented in this paper will go through various versions. We will use dates for versioning. The initial version is dated April 1, 2019, and might be referred to as the April fool’s version.

Every time a problem with one of the programs in this benchmark is discovered, we will modify the program to remove the problem, and give the benchmark a new version date. In that case we will add a short description to this section of the problem, how it was discovered and how the program was changed to remove the problem. This means that this section will be some kind of high level changelog.

Note that bad behavior outside the intended domain of behavior of a program does not count as a problem. For example, integer overflow in the earlier factorial programs in Section 2 is not a problem. This should be handled by a precondition of the correctness statement of the code, and does not merit modification of the code in the benchmark.

8 Discussion

We can imagine different reactions to the collection of programs that we present here:

• •

These programs are too easy.

• •

These programs are too hard.

• •

These programs are not too easy or too hard, but not interesting.

In the first case we would like to see how to verify them. If they are easy, showing how to do that should not be much work, right? In the second case we would like to know how far the technology currently reaches. We intentionally provided a spectrum from very small fragments to larger pieces of code, so if you have the second reaction then just show us how to do the easier ones.

However, in the third case we disagree. This is based on actual programs from the GNU project, and as such are representative of real C programming. Why is it not interesting to be able to verify what to us are characteristic C programs?

It was tempting to also include programs in our benchmark that are cute and/or dazzling. (The square root approximation by bit shifting in Section 6.2 was borderline in this respect.) For instance, consider two possible additions to the factorial section, the first being a surprising application of the preprocessor:

(it turns out that the factorial is calculated here at compile time), and the second being a price winning submission to the international obfuscated C code contest (it implements a functional language and then does the recursion by evaluating Church’s $Y$-combinator.) However, we do not consider these two programs representative of real life C programming, so we resisted the temptation to include them in our benchmark.

There are twenty-five programs in this paper, and there are multiple frameworks for formal C verification out there, like the ones described in [1], [6], [7], [11] and [15]. We think this could be a great source for student projects. Just say, for example: ‘prove the correctness of program number three in framework number one’ (actually something close to that one already has been done, see the slides of [23]). That way we will get a good comparison of what are the strengths and weaknesses of the different current approaches for formal C verification.

9 Related work

Benchmarks/competitions very similar to the one presented in this paper already exist:

• •

VACID-0 [19]:

https://archive.codeplex.com/?p=vacid

• •

Verfified Software Competition [9, 16].

• •

VerifyThis Competition:

http://www.pm.inf.ethz.ch/research/verifythis.html

The main difference from the benchmark presented here is that they do not target C explicitly. Yet, they sometimes use C code in their statements, and sometimes participants are using C for their solutions.

There are also benchmarks that are about specific programming languages, which often have a C section, like for example:

• •

Collection of Verification Tasks of the SoSy-Lab at the Ludwig-Maximilian University in Munich:

https://github.com/sosy-lab/sv-benchmarks/tree/master/c

However, in that case the focus is not so much on formally proving that programs are fully correct, but on benchmarking the performance of non-interactive tools for discovering problems in the programs.

Acknowledgments

Thanks to Jean-Christophe Filliâtre for many helpful comments.