Software Verification

When we talk about software verification, it’s best to show a small example found at Google’s research blog. Let’s look at a Java implementation of binary search:

public static int binarySearch(int[] a, int key) {
	int low = 0;
	int high = a.length - 1;

	while (low <= high) {
		int mid = (low + high) / 2;
		int midVal = a[mid];

		if (midVal < key)
			low = mid + 1;
		else if (midVal > key)
			high = mid - 1;
		else
			return mid; // key found
	}
	return -(low + 1);  // key not found.
}

At first sight the implementation seems to be perfectly fine. But let’s take a closer look at line 6:

int mid = (low + high) / 2;

This line fails for large values of ‘low’ and ‘high’. To be precise: The line fails when . In such a case we have an integer overflow in the addition, return a negative number as result and finally get an IndexOutOfBounds exception.

Our aim is to detect such errors beforehand by performing static code analysis. One possible way to do so is bounded model checking (BMC). In BMC we convert a program into a Boolean formula and add some constraints we want to check (e.g. the lack of integer overflows). The whole formula can then be passed to a SAT solver. If the formula is unsatisfiable, the constraints hold for the given program. If the formula is satisfiable, one of the constraints does not hold and the satisfying assignment of the problem represents an input leading to an error.