ture. Therefore, the model is a counterexample of the conjecture, and when
the current value of b is false, nothing
can be said about its value after the execution of the statement. The result
of these three proof attempts is then
used to replace the statement count =
count +
1; by if (b) b = false; else
b = *;. A finite state model checker can
now be used on the Boolean program
and will establish that b is always true
when control reaches this statement,
verifying that calls to lock() are balanced with calls to unlock() in the
original program.
Static program analysis. Static program analysis tools work like dynamic-symbolic-execution tools, checking
feasibility of program paths. On the
other hand, they never require executing programs and can analyze software
libraries and utilities independently of
how they are used. One advantage of
using modern SMT solvers in static program analysis is they accurately capture
the semantics of most basic operations
used by mainstream programming languages. The program fragment in Program 3. 5 illustrates the need for static
program analysis to use bit-precise reasoning, searching for an index in a sorted array arr containing a key.
The assert statement is a precon-
dition for the procedure, restricting the
input to fall within the bounds of the
array arr. The program performs sev-
eral operations involving arithmetic, so
a theory and corresponding solver that
understands arithmetic is arguably a
good match. However, it is important
for software-analysis tools to take into
account that languages (such as Java,
C#, and C/C++) all use fixed-width bit-
vectors as representation for values of
type int, meaning the accurate theory
for int is two-complements modular
arithmetic. Assuming a bit-width of
32b, the maximal positive 32b integer
is 231− 1, and the smallest negative 32b
integer is −231. If both low and high are
230, low + high evaluates to 231, which is
treated as the negative number −231. The
presumed assertion 0 ≤ mid < high does
therefore not hold. Fortunately, several
modern SMT solvers support the theory
of “bit-vectors,” accurately capturing
the semantics of modular arithmetic.
The bug does not escape an analysis
based on the theory of bit-vectors. Such
analysis would check that the array read
arr[mid] is within bounds during the
first iteration by checking the formula
figure 3. axioms for sub.
( ∀ x: sub(x, x))
( ∀ x,y,z: sub(x, y) ∧ sub(y, z) → sub(x, z))
( ∀ x,y: sub(x, y) ∧ sub(y, x) → x = y)
( ∀ x,y,z: sub(x, y) ∧ sub(x, z) → sub(y, z) ∨ sub(z, y))
( ∀ x,y: sub(x, y) → sub(array-of(x), array-of(y)))
(low > high ∨ 0 ≤ low < high < arr.length)
∧ (low ≤ high → 0 ≤ (low + high)/2 < arr.
length)
As in the case of code fragment 3. 5, the
formula is not valid. The values low =
high = 230, arr.length = 230+ 1 provide a counterexample. The use of SMT
solvers for bit-precise static-analysis
tools is an active area of research and
development in Microsoft Research.
Integration with the solver Z314 and the
static analysis tool PREfix led to the automatic discovery of several overflow-related bugs in Microsoft’s codebase.
Program verification. The ideal of
verified software is a long-running
quest since Robert Floyd and C.A.R.
Hoare introduced (in the late 1960s)
program verification by assigning logical assertions to programs. Extended
Program 3. 5. Binary search.
int binary_search(
int[] arr, int low, int high, int key) {
assert (low > high || 0 <= low < high);
while (low <= high) {
//Find middle value
int mid = (low + high)/2;
assert (0 <= mid < high);
int val = arr[mid];
//Refine range
if (key == val) return mid;
if (val > key) low = mid+ 1;
else high = mid– 1;
}
return – 1;
}
static checking uses the methods developed for program verification but in
the more limited context of checking
absence of runtime errors. The SMT
solver Simplify16 was developed in the
context of the extended static-checking
systems ESC/Modula 3 and ESC/Java.
21
This work was and continues to be
the inspiration for several subsequent
verification tools, including Why19 and
Boogie.
3 These systems are actively
used as bridges from several different
front ends to SMT-solver back ends; for
example, Boogie is used as a back end
for systems that verify code from languages (such as an extended version of
C# called Spec#), as well as low-level
systems code written in C. Current
practice indicates that a lone software
developer can drive these tools to verify properties of large codebases with
several hundred thousand lines of
code. A more ambitious project is the
Verifying C-Compiler system,
11
targeting functional correctness properties
of Microsoft’s Viridian Hyper-Visor.
The Hyper-Visor is a relatively small
( 100,000 lines) operating-system layer,
yet formulating and establishing correctness properties is a challenge. The
entire verification effort for this layer is
estimated by Microsoft to take around
60 programmer years.
Program-verification applications
often use theories not already supported by existing specialized solvers
but that are supported indirectly using
axiomatizations with quantifiers. As an
example of such a theory, in object-ori-ented-type systems used for Java and
C#, it is the case that objects are related using a single inheritance scheme;
that is, every object inherits from at
most one unique immediate parent.
To illustrate the theory, let array-of(x)
be the array type constructor for arrays
of values of type x. In some programming languages, if x is a subtype of y,
then array-of(x) is a subtype of array-
