IA159 Formal Methods for Software Analysis
Symbolic Execution and Applications
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
focus
symbolic execution
automated whitebox fuzz testing
bounded model checking
sources
J. C. King: Symbolic Execution and Program Testing, Communications of
ACM, 1976.
P. Godefroid, M. Y. Levin, and D. Molnar: Automated whitebox fuzz testing,
NDSS 2008.
Special thanks to Marek Trtík for providing me his slides.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 2/53
Motivation
1 procedure sum (a, b, c) {
2 x = a + b;
3 y = b + c;
4 z = x + y − b;
5 return z;
6 }
Testing checks that the program behaves correctly on selected inputs
sum (1, 1, 1) =
sum (1, 2, 3) =
. . .
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 3/53
Motivation
1 procedure sum (a, b, c) {
2 x = a + b;
3 y = b + c;
4 z = x + y − b;
5 return z;
6 }
Testing checks that the program behaves correctly on selected inputs
sum (1, 1, 1) = 3
sum (1, 2, 3) = 6
. . .
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 4/53
Motivation
1 procedure sum (a, b, c) {
2 x = a + b;
3 y = b + c;
4 z = x + y − b;
5 return z;
6 }
We can execute the program with symbols α1, α2, α3 representing arbitrary input
values
sum (α1, α2, α3) =
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 5/53
Motivation
1 procedure sum (a, b, c) {
2 x = a + b;
3 y = b + c;
4 z = x + y − b;
5 return z;
6 }
We can execute the program with symbols α1, α2, α3 representing arbitrary input
values
sum (α1, α2, α3) = α1 + α2 + α3
→ symbolic execution
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 6/53
Symbolic execution semantics in general
Each programming language has an execution semantics describing
the data objects which program variables may represent
how statements manipulate data objects
how control flows through the statements of a program
In symbolic execution semantics
real data objects can be represented by symbols
basic operators of the language are extended to accept symbolic input and
produce symbolic output
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 7/53
Simple programming language
Consider the following programming language
all program variables are of type unbounded signed integer
input can be obtained by procedure parameters, global variables, or read
operations
arithmetic expressions may contain only operators +, −, ∗
commands:
assignment <var> := <expr>
goto <label>
if-then-else with condition <expr> ≥ 0
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 8/53
Semantics of the language
Standard execution semantics
data objects = signed integers
. . .
Symbolic execution semantics
besides integers, we can use symbols from the list α1, α2, α3, . . . to represent
some data objects
the only opportunity to introduce symbolic data objects is as inputs to the
program
the evaluation rules for arithmetic expressions used in assignments and if
statements must be extended to handle symbolic values
goto works exactly as in normal executions
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 9/53
Extending rules for expressions and if statement
Values of expressions and variables are integer polynomials over the symbols
α1, α2, . . ..
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 10/53
Extending rules for expressions and if statement
Values of expressions and variables are integer polynomials over the symbols
α1, α2, . . ..
Although if statement does not change the state of program variables, it plays a
key role in the definition of symbolic semantics.
We extend the system state by path condition pc, which is a conjunction of
inequalities of the form R ≥ 0 or ¬(R ≥ 0), where R is a polynomial over
α1, α2, . . ..
pc is initially set to true
pc can only be modified when executing if statements
Intuitively, pc accumulates conditions navigating the execution along the current
path.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 11/53
Extending path condition
Let q be an inequality resulting from substituting values of variables into condition
of an if statement.
Assuming pc ̸≡ false, at most one of the following implications can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
A formula φ is valid if and only if ¬φ is unsatisfiable. Hence, SMT solvers are used
to check validity.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 12/53
Extending path condition
Let q be an inequality resulting from substituting values of variables into condition
of an if statement.
Assuming pc ̸≡ false, at most one of the following implications can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
A formula φ is valid if and only if ¬φ is unsatisfiable. Hence, SMT solvers are used
to check validity.
If one implication is valid, then we speak about non-forking execution and pc is not
changed.
If (a) is valid, the execution continues by then branch.
If (b) is valid, the execution continues by else branch.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 13/53
Extending path condition
Let q be an inequality resulting from substituting values of variables into condition
of an if statement.
Assuming pc ̸≡ false, at most one of the following implications can be valid:
(a) pc =⇒ q
(b) pc =⇒ ¬q
A formula φ is valid if and only if ¬φ is unsatisfiable. Hence, SMT solvers are used
to check validity.
When neither (a) nor (b) is valid, then we speak about forking execution. The
current execution forks into two independent ones, since both branches are
possible. Path conditions of resulting executions are updated as follows:
pc ← pc ∧ q for then branch
pc ← pc ∧ ¬q for else branch
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 14/53
Example
1 procedure power (x, y) {
2 z := 1;
3 j := 1;
4 lab: if (y − j ≥ 0) then {
5 z := z ∗ x;
6 j := j + 1;
7 goto lab;
8 }
9 return z;
10 }
(draw symbolic execution on the whiteboard)
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 15/53
Path condition is always satisfiable
Clearly, every path condition corresponds exactly to one execution path and vice
versa.
Theorem
At each point of every symbolic execution pc ̸≡ false.
Proof: Initially, pc is set to true. Further, pc is modified only at forking executions,
using assignments of the form pc ← pc ∧ q and pc ← pc ∧ ¬q.
Forking execution implies that pc =⇒ ¬q is not valid. Hence, ¬(pc =⇒ ¬q) is
satisfiable. As pc ∧ q ≡ ¬(pc =⇒ ¬q), pc ∧ q is also satisfiable.
The case pc ∧ ¬q is similar.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 16/53
Symbolic execution tree
The execution paths followed during the symbolic execution of a procedure can be
expressed by symbolic execution tree.
executed statement = a node labeled with the statement number
transition between executed statements = a directed arc connecting the
corresponding nodes
for each forking if statement execution there are two outgoing arcs labeled
with T and F for then and else branch, respectively
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 17/53
Symbolic execution tree for power(α1, α2)
1
2
3
4
5
9
6
7
4
5
9
T
F
T
F
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 18/53
Symbolic execution tree
Lemma
For each terminal leaf in the tree there exists particular non-symbolic input, which
will trace the same path.
Proof: Every input satisfying the corresponding pc trace the same path. As pc is
always satisfiable, there exists such an input.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 19/53
Symbolic execution tree
Lemma
For each terminal leaf in the tree there exists particular non-symbolic input, which
will trace the same path.
Proof: Every input satisfying the corresponding pc trace the same path. As pc is
always satisfiable, there exists such an input.
Lemma
Path conditions associated with any two terminal leaves are distinct,
i.e. pc1 ∧ pc2 ≡ false.
Proof: The two paths leading from the root to two different terminal nodes have a
unique forking node where the paths diverge. At that forking node some q was
added to one while ¬q to the other. Since q ∧ ¬q ≡ false, the lemma holds.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 20/53
Commutativity
If one normally executes a program with a specific set of integers {ji}, the result
will be the same as executing it symbolically (using a set of {αi}) and then
instantiating the symbolic results, i.e., assigning {ji} to {αi}.
P,{αi},{ji}
P,{αi} ← {ji}
P({αi}),{ji}
P({ji})
set parameters to integer values
symbolic execution
standard execution
substitute into symbolic result
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 21/53
Memoryless version of symbolic execution
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 22/53
Applications in verification
Programs can be enriched with assume(φ) and assert(φ) statements. When
symbolic execution passes through
assume(φ), it executes pc ← pc ∧ φ.
assert(φ) and pc =⇒ φ is not valid, it reports an error.
With these constructs, symbolic execution can be used with a modification of
Floyd’s proof method to prove program correctness.
This application is straightforward for any program whose symbolic execution tree
is finite.
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 23/53
Practical issues
deciding validity or satisfiability of formulas can be expensive or even
impossible (e.g. for our simple language with unbounded data types)
in practice, symbolic execution uses expressions and formulas over bitvector
theory (operations and relations correspond to CPU instructions,
e.g. artihmetic operations with overflows, bitwise operations, etc.), where
validity and satisfiability are decidable (but expensive)
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 24/53
Practical issues
variable storage referencing problem
when i is dependent on input, then A[i] can point to various locations in
memory
unsatisfactory solution:
handle A[i] as ITE(i = 1, A[1], ITE(i = 2, A[2], . . .))
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 25/53
Practical issues
variable storage referencing problem
when i is dependent on input, then A[i] can point to various locations in
memory
unsatisfactory solution:
handle A[i] as ITE(i = 1, A[1], ITE(i = 2, A[2], . . .))
other memory related problems
reading/writing via pointers
comparison of addresses (inner program nondeterminism)
allocation of memory blocks of symbolic size
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 26/53
Practical issues
variable storage referencing problem
when i is dependent on input, then A[i] can point to various locations in
memory
unsatisfactory solution:
handle A[i] as ITE(i = 1, A[1], ITE(i = 2, A[2], . . .))
other memory related problems
reading/writing via pointers
comparison of addresses (inner program nondeterminism)
allocation of memory blocks of symbolic size
solution: fully symbolic memory model
performance issues
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 27/53
Practical issues
path explosion problem
the number of branches in the symbolic execution tree can be extremely high or
even infinite
typical for program cycles with the number of iterations depending on the input
(symbolic execution forks again and again)
construction of full symbolic execution tree is often infeasible
issues with complex arithmetic operations (e.g. in hashing, encryption or
decryption), calls to the operating system and libraries
practical solutions
concretization
concolic execution
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 28/53
Concolic execution
concolic = concrete + symbolic
program is executed on a real input and on symbolic input simultaneously
symbolic execution does not fork, it always follows the concrete execution and
computes pc
if a symbolic value is not available, we can switch to a concrete one
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 29/53
Real applications
typical applications
bug finding
test generation
analysis of abstract error traces
often combined with other techniques
used in many tools including Klee, PEX, SAGE, SLAM, Ultimate Automizer,
Symbiotic
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 30/53
Automated whitebox fuzz testing
Automated whitebox fuzz testing
an example of modern and sophisticated testing method
implemented in SAGE (Scalable, Automated, Guided Execution)
discovered 30+ new bugs in large-shipped (and thus intensively tested)
file-reading Windows applications including image processors, media players,
file decoders
combines fuzz testing and symbolic execution
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 32/53
Key ideas
symbolic execution is expensive compared to running tests
thus we want to generate as many new inputs from one symbolic execution as
possible
input for the next symbolic execution is selected by some scoring function
applied to all generated inputs
in particular, the input that explored the most (so-far uncovered) pieces of
code is chosen for the next symbolic execution
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 33/53
The main algorithm
1 procedure GenerateInputs(inputSeed)
2 inputSeed.bound ← 0
3 workList ← {inputSeed}
4 Run&Check(program, inputSeed)
5 while workList ̸= ∅ do
6 input ← PickFirstItem(workList)
7 childInputs ← ExpandExecution(input)
8 foreach newInput ∈ childInputs do
9 Run&Check(program, newInput)
10 Score(newInput)
11 workList ← workList ∪ {newInput}
Score(newInput) counts the newly covered blocks
workList is ordered by the score of inputs
PickFirstItem(workList) returns the input with the highest score
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 34/53
Application of symbolic execution
1 procedure ExpandExecution(input)
2 childInputs ← ∅
3 PC ← SymbolicExecution(program, input)
4 for j ← input.bound to |PC| − 1 do
5 if j−1
i=0 PC[i] ∧ ¬PC[j] has solution M then
6 newInput ← Combine(input, M)
7 newInput.bound ← j
8 childInputs ← childInputs ∪ {newInput}
9 return childInputs
Combine(input, M)
creates a new input from the original input and M
Combine("abcde", input[3] → "F") returns "abcFe"
path conditions are represented as arrays PC of conjuncts
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 35/53
Example
1 void top(char input[4]) {
2 int cnt=0;
3 if (input[0] == ’b’) cnt++;
4 if (input[1] == ’a’) cnt++;
5 if (input[2] == ’d’) cnt++;
6 if (input[3] == ’!’) cnt++;
7 if (cnt >= 3) abort(); // error
8 }
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 36/53
Example
1 void top(char input[4]) {
2 int cnt=0;
3 if (input[0] == ’b’) cnt++;
4 if (input[1] == ’a’) cnt++;
5 if (input[2] == ’d’) cnt++;
6 if (input[3] == ’!’) cnt++;
7 if (cnt >= 3) abort(); // error
8 }
0 1 1 2 1 2 2 3 1 2 2 3 2 3 3 4
good
goo!
godd
god!
gaod
gao!
gadd
gad!
bood
boo!
bodd
bod!
baod
bao!
badd
bad!
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 37/53
Notes
the algorithm can be parallelized: only workList and the overall block coverage
need to be shared
SAGE recovers easily from divergencies (situations when an execution
deviates from the assumed execution path) induced e.g. by inner program
nondeterminism
SAGE runs 24/7 on large clusters, available for Microsoft developers
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 38/53
Bounded model checking
Bounded model checking (BMC)
a technique for finding bugs
proves correctness only very rarely
similar to symbolic execution, but creates one SMT query
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 40/53
Bounded model checking (BMC)
a technique for finding bugs
proves correctness only very rarely
similar to symbolic execution, but creates one SMT query
workflow
1 unwind all loops and recursion to a given bound k
2 compute the error reaching formula in unwound program
3 check satisfiability of the formula
4 if satisfiable
5 then bug found
6 else if the bound is not reachable
7 then the program is correct
8 else unknown (increase bound and goto 1)
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 41/53
Example
original program
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
while (i < n) {
v = input();
s += v;
++i;
}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 42/53
Example
original program unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
while (i < n) {
v = input();
s += v;
++i;
}
assert(s >= v);
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 43/53
Example
unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 44/53
Example
unwound program for k = 3 unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ ((i1 ≥ n1 ∧ s1 < v1) ∨
∨ (i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ ((i2 ≥ n1 ∧ s2 < v2) ∨
∨ (i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ ((i3 ≥ n1 ∧ s3 < v3) ∨
∨ (i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 ≥ n1 ∧ s4 < v4))))))
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 45/53
Example
unwound program for k = 3 unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned char s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ ((i1 ≥ n1 ∧ s1 < v1) ∨
∨ (i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ ((i2 ≥ n1 ∧ s2 < v2) ∨
∨ (i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ ((i3 ≥ n1 ∧ s3 < v3) ∨
∨ (i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 ≥ n1 ∧ s4 < v4))))))
satisfiable
variable types are considered
bitvector arithmetic is used
n1 = 2
v1 = 0 s1 = 0 i1 = 0
v2 = 224 s2 = 224 i2 = 1
v3 = 63 s3 = 31 i3 = 2
bug found!
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 46/53
Example 2
original program
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
while (i < n) {
v = input();
s += v;
++i;
}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 47/53
Example 2
original program unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
while (i < n) {
v = input();
s += v;
++i;
}
assert(s >= v);
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 48/53
Example 2
unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 49/53
Example 2
unwound program for k = 3 unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ ((i1 ≥ n1 ∧ s1 < v1) ∨
∨ (i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ ((i2 ≥ n1 ∧ s2 < v2) ∨
∨ (i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ ((i3 ≥ n1 ∧ s3 < v3) ∨
∨ (i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 ≥ n1 ∧ s4 < v4))))))
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 50/53
Example 2
unwound program for k = 3 unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ ((i1 ≥ n1 ∧ s1 < v1) ∨
∨ (i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ ((i2 ≥ n1 ∧ s2 < v2) ∨
∨ (i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ ((i3 ≥ n1 ∧ s3 < v3) ∨
∨ (i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 ≥ n1 ∧ s4 < v4))))))
unsatisfiable
is the bound reachable?
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 < n1
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 51/53
Example 2
unwound program for k = 3 unwound program for k = 3
unsigned char n = input();
if (n == 0) {return 0};
unsigned char v = 0;
unsigned int s = 0;
unsigned int i = 0;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
v = input();
s += v;
++i;
if (i < n) {
bound_reached();}}}}
assert(s >= v);
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ ((i1 ≥ n1 ∧ s1 < v1) ∨
∨ (i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ ((i2 ≥ n1 ∧ s2 < v2) ∨
∨ (i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ ((i3 ≥ n1 ∧ s3 < v3) ∨
∨ (i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 ≥ n1 ∧ s4 < v4))))))
unsatisfiable
is the bound reachable?
n1 > 0 ∧ v1 = 0 ∧ s1 = 0 ∧ i1 = 0 ∧
∧ i1 < n1 ∧ s2 = s1 + v2 ∧ i2 = i1 + 1 ∧
∧ i2 < n1 ∧ s3 = s2 + v3 ∧ i3 = i2 + 1 ∧
∧ i3 < n1 ∧ s4 = s3 + v4 ∧ i4 = i3 + 1 ∧
∧ i4 < n1
satisfiable =⇒ bound reachable
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 52/53
Notes on BMC
very efficient in finding bugs
constant propagation can simplify the program and the formula
implemented for example in CBMC
tool for bounded model checking of C and C++ programs
supports C89, C99, most of C11 and most extensions of gcc and Visual Studio
the winner of SV-COMP 2014
https://www.cprover.org/cbmc/
a version for Java programs called JBMC
IA159 Formal Methods for Software Analysis: Symbolic Execution and Applications 53/53