IA159 Formal Methods for Software Analysis
Bounded Model Checking, k-Induction
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
focus
memoryless version of symbolic execution
bounded model checking (BMC)
k-induction
source
A. F. Donaldson, L. Haller, D. Kroening, and P. Rümmer: Software Verification
Using k-Induction, SAS 2011.
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 2/30
Memoryless version of symbolic execution
does not use symbolic memory, the assignments are stored to path condition
to do that, we need to consider another instance of each variable after each
assignment to it and remeber its current instance
let ver : Vars → N be the function keeping the current instances
initially, ver(x) = 1 for each x ∈ Vars
a
b
y = 2*x+y+5;
path condition pc
function ver
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 3/30
Memoryless version of symbolic execution
does not use symbolic memory, the assignments are stored to path condition
to do that, we need to consider another instance of each variable after each
assignment to it and remeber its current instance
let ver : Vars → N be the function keeping the current instances
initially, ver(x) = 1 for each x ∈ Vars
a
b
y = 2*x+y+5;
path condition pc
function ver
path condition pc ∧ yver(y)+1 = 2 ∗ xver(x) + yver(y) + 5
function ver with incresed value of ver(y) by one
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 4/30
Memoryless version of symbolic execution
does not use symbolic memory, the assignments are stored to path condition
to do that, we need to consider another instance of each variable after each
assignment to it and remeber its current instance
let ver : Vars → N be the function keeping the current instances
initially, ver(x) = 1 for each x ∈ Vars
a
b
y = 2*x+y+5;
path condition pc
function ver
path condition pc ∧ yver(y)+1 = 2 ∗ xver(x) + yver(y) + 5
function ver with incresed value of ver(y) by one
a
b
y = *;
path condition pc
function ver
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 5/30
Memoryless version of symbolic execution
does not use symbolic memory, the assignments are stored to path condition
to do that, we need to consider another instance of each variable after each
assignment to it and remeber its current instance
let ver : Vars → N be the function keeping the current instances
initially, ver(x) = 1 for each x ∈ Vars
a
b
y = 2*x+y+5;
path condition pc
function ver
path condition pc ∧ yver(y)+1 = 2 ∗ xver(x) + yver(y) + 5
function ver with incresed value of ver(y) by one
a
b
y = *;
path condition pc
function ver
path condition pc
function ver with incresed value of ver(y) by one
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 6/30
Memoryless version of symbolic execution
does not use symbolic memory, the assignments are stored to path condition
to do that, we need to consider another instance of each variable after each
assignment to it and remeber its current instance
let ver : Vars → N be the function keeping the current instances
initially, ver(x) = 1 for each x ∈ Vars
a
b
y = 2*x+y+5;
path condition pc
function ver
path condition pc ∧ yver(y)+1 = 2 ∗ xver(x) + yver(y) + 5
function ver with incresed value of ver(y) by one
a
b
y = *;
path condition pc
function ver
path condition pc
function ver with incresed value of ver(y) by one
symbolic execution of branching statements is modified similarly
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 7/30
Bounded model checking (BMC)
Bounded model checking (BMC)
a technique for finding bugs
proves correctness only very rarely
similar to memoryless symbolic execution, but creates one SMT query
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 9/30
Bounded model checking (BMC)
a technique for finding bugs
proves correctness only very rarely
similar to memoryless symbolic execution, but creates one SMT query
workflow
1 unwind all loops and recursion k-times for a given bound k
2 compute the error reaching formula φ from the unwound program
3 if φ is satisfiable then
4 return bug found
5 else
6 compute the bound reaching formula ψ from the unwound program
7 if the ψ is unsatisfiable then
8 return the program is correct
9 else
10 return unknown (increase bound and start again)
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 10/30
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: Bounded Model Checking, k-Induction 11/30
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: Bounded Model Checking, k-Induction 12/30
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: Bounded Model Checking, k-Induction 13/30
Example
unwound program for k = 3 error reaching formula φ
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: Bounded Model Checking, k-Induction 14/30
Example
unwound program for k = 3 error reaching formula φ
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: Bounded Model Checking, k-Induction 15/30
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: Bounded Model Checking, k-Induction 16/30
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: Bounded Model Checking, k-Induction 17/30
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: Bounded Model Checking, k-Induction 18/30
Example 2
unwound program for k = 3 error reaching formula φ
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: Bounded Model Checking, k-Induction 19/30
Example 2
unwound program for k = 3 error reaching formula φ
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
bound reaching formula ψ
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: Bounded Model Checking, k-Induction 20/30
Example 2
unwound program for k = 3 error reaching formula φ
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
bound reaching formula ψ
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 =⇒ unknown (bound reachable)
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 21/30
Notes on BMC
very efficient in finding bugs
uses a sort of SSA when constructing the formula
constant propagation can simplify the program and the formula and it can
reveal that the bound is unreachable
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: Bounded Model Checking, k-Induction 22/30
k-induction
k-induction
extension of BMC that can prove correctness more often
very successful on symbolic transition systems
to prove program correctness, we show
1 base case:
all feasible paths starting in an initial state of length at most k are correct
2 induction step:
each feasible path of length k + 1 that has a correct prefix of length k is also
correct
if the base case fails, we found a bug
if the induction step fails, we can increase k and try again
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 24/30
k-induction
extension of BMC that can prove correctness more often
very successful on symbolic transition systems
to prove program correctness, we show
1 base case:
all feasible paths starting in an initial state of length at most k are correct
2 induction step:
each feasible path of length k + 1 that has a correct prefix of length k is also
correct
if the base case fails, we found a bug
if the induction step fails, we can increase k and try again
the idea can be applied to programs in different ways
k-induction on single-loop programs
k-induction does semantically the same as backward symbolic execution
M. Chalupa and J. Strejˇcek: Backward Symbolic Execution with Loop Folding,
SAS 2021.
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 25/30
k-induction on single-loop programs
n,x,i = *,0,0;
a,b,c = 1,2,3;
while (i < n) {
assert(a != b);
a,b,c = b,c,a;
i++;
}
assert(x = 0);
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 26/30
k-induction on single-loop programs
n,x,i = *,0,0;
a,b,c = 1,2,3;
while (i < n) {
assert(a != b);
a,b,c = b,c,a;
i++;
}
assert(x = 0);
n,x,i = *,0,0;
a,b,c = 1,2,3;
assume i < n;
assert a ̸= b;
a,b,c = b,c,a;
i = i+1;
assume i ≥ n;
assert x = 0;
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 27/30
k-induction on single-loop programs
n,x,i = *,0,0;
a,b,c = 1,2,3;
while (i < n) {
assert(a != b);
a,b,c = b,c,a;
i++;
}
assert(x = 0);
n,x,i = *,0,0;
a,b,c = 1,2,3;
assume i < n;
assert a ̸= b;
a,b,c = b,c,a;
i = i+1;
assume i ≥ n;
assert x = 0;
n,x,i = *,0,0;
a,b,c = 1,2,3;
assume i < n;
assert a ̸= b;
a,b,c = b,c,a;
i = i+1;
B:
B
B
assume i ≥ n;
assert x = 0;
base case (= BMC)
for k = 3
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 28/30
k-induction on single-loop programs
n,x,i = *,0,0;
a,b,c = 1,2,3;
while (i < n) {
assert(a != b);
a,b,c = b,c,a;
i++;
}
assert(x = 0);
n,x,i = *,0,0;
a,b,c = 1,2,3;
assume i < n;
assert a ̸= b;
a,b,c = b,c,a;
i = i+1;
assume i ≥ n;
assert x = 0;
n,x,i = *,0,0;
a,b,c = 1,2,3;
assume i < n;
assert a ̸= b;
a,b,c = b,c,a;
i = i+1;
B:
B
B
assume i ≥ n;
assert x = 0;
base case (= BMC)
for k = 3
n,x,i = *,*,*;
a,b,c = *,*,*;
assume i < n;
assume a ̸= b;
a,b,c = b,c,a;
i = i+1;
B′
:
B′
B′
B
assume i ≥ n;
assert x = 0;
induction step for k = 3
IA159 Formal Methods for Software Analysis: Bounded Model Checking, k-Induction 29/30
The End