IA159 Formal Methods for Software Analysis
Verification via Automata, Symbolic Execution, and Interpolation
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
ULTIMATEfocus
basic principle
interpolation
example
sources
M. Heizmann, J. Hoenicke, A. Podelski: Software Model Checking for People
Who Love Automata, CAV 2013.
M. Heizmann, J. Hoenicke, A. Podelski: Termination Analysis by Learning
Terminating Programs, CAV 2014.
Special thanks to M. Heizmann for providing me with his slides.
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 2/47
Programs as languages
New view on programs
A program defines a language over program statements.
alphabet = the set of program statements
finite automaton = control flow graph
accepting states = error locations
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 3/47
Programs as languages
New view on programs
A program defines a language over program statements.
alphabet = the set of program statements
finite automaton = control flow graph
accepting states = error locations
int z = 0;
int x = 0;
while (x < 20) {
if (i != 0) { z++; }
x++;
}
assert(z <= 5);
0
1
2
3
4 5
6
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 4/47
The goal
such an automaton accepts error traces
not all error traces are feasible
The goal
To decide whether there exists a feasible error trace accepted by the automaton.
The program is correct iff all error traces accepted by the automaton are infeasible.
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 5/47
The algorithm
program P
automaton R
L(R) = ∅
L(P) ⊆ L(R)?
P is correct
is π feasible?
(symbolic execution)
P is incorrect
+ feasible error trace π
yes
no
pick an error trace
π ∈ L(P) ∖ L(R)
yes
no
build an automaton R′
s.t. L(R′
) = {π}
generalize R′
to accept more infeasible traces
change R to accept L(R) ∪ L(R′
)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 6/47
The algorithm
program P
automaton R
L(R) = ∅
L(P) ⊆ L(R)?
P is correct
is π feasible?
(symbolic execution)
P is incorrect
+ feasible error trace π
yes
no
pick an error trace
π ∈ L(P) ∖ L(R)
yes
no
build an automaton R′
s.t. L(R′
) = {π}
generalize R′
to accept more infeasible traces
change R to accept L(R) ∪ L(R′
)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 7/47
Craig interpolation
Theorem (William Craig, 1957)
Let φ, ψ be two first-order formulae such that φ =⇒ ψ. Then there exists a first
order-formula θ called interpolant such that
all non-logical symbols (i.e., variables and uninterpreted function and
predicate symbols) in θ occur in both φ and ψ,
φ =⇒ θ =⇒ ψ.
φ ψ
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 8/47
Craig interpolation
Theorem (William Craig, 1957)
Let φ, ψ be two first-order formulae such that φ =⇒ ψ. Then there exists a first
order-formula θ called interpolant such that
all non-logical symbols (i.e., variables and uninterpreted function and
predicate symbols) in θ occur in both φ and ψ,
φ =⇒ θ =⇒ ψ.
φ ψθ
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 9/47
Craig interpolation
Theorem (William Craig, 1957)
Let φ, ψ be two first-order formulae such that φ =⇒ ψ. Then there exists a first
order-formula θ called interpolant such that
all non-logical symbols (i.e., variables and uninterpreted function and
predicate symbols) in θ occur in both φ and ψ,
φ =⇒ θ =⇒ ψ.
φ ¬ψ
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 10/47
Craig interpolation
Theorem (William Craig, 1957)
Let φ, ψ be two first-order formulae such that φ =⇒ ψ. Then there exists a first
order-formula θ called interpolant such that
all non-logical symbols (i.e., variables and uninterpreted function and
predicate symbols) in θ occur in both φ and ψ,
φ =⇒ θ =⇒ ψ.
φ ¬ψθ
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 11/47
Example: program
int z = 0;
int x = 0;
while (x < 20) {
if (i != 0) { z++; }
x++;
}
assert(z <= 5);
0
1
2
3
4 5
6
Err
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 12/47
Example: error trace
int z = 0;
int x = 0;
while (x < 20) {
if (i != 0) { z++; }
x++;
}
assert(z <= 5);
0
1
2
3
4 5
6
Err
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 13/47
Example: error path
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
0
1
2
3
4 5
6
Err
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 14/47
Example: feasability analysis
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
symbolic execution produces
z = 0 ∧ x = 0 ∧ x ≥ 20 ∧ z > 5 ≡ false
=⇒ the error trace is infeasible
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 15/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 16/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
true
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 17/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true ∧ z = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 18/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
true ∧ z = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
z = 0
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 19/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0 ∧ x = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 20/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0 ∧ x = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
z = 0
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 21/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0 ∧ x ≥ 20
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 22/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
z = 0 ∧ x ≥ 20
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
z = 0
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 23/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
z = 0 ∧ z > 5
true
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 24/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
z = 0 ∧ z > 5
true
false
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 25/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 26/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
true
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 27/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true ∧ z = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 28/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
true ∧ z = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
true
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 29/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
true ∧ x = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 30/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
x = 0
true ∧ x = 0
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
x = 0
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 31/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
x = 0
x = 0 ∧ x ≥ 20
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 32/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
x = 0
false
x = 0 ∧ x ≥ 20
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
false
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 33/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
x = 0
false
false ∧ z > 5
true
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 34/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
z = 0
z = 0
z = 0
false
true
true
x = 0
false
false
false ∧ z > 5
true
false
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 35/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
x = 0
false
false
true
x = 0
false
Σ = {z = 0;, x = 0;, (x >= 20),
(x < 20), (i == 0), (i != 0),
z++;, x++;, (z > 5)}
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 36/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
x = 0
false
false
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ = {z = 0;, x = 0;, (x >= 20),
(x < 20), (i == 0), (i != 0),
z++;, x++;, (z > 5)}
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 37/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
x = 0
false
false
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ ∖ {x++;, (x >= 20)}
Σ = {z = 0;, x = 0;, (x >= 20),
(x < 20), (i == 0), (i != 0),
z++;, x++;, (z > 5)}
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 38/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
x = 0
false
false
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ ∖ {x++;, (x >= 20)}
(x >= 20)
x++;
Σ = {z = 0;, x = 0;, (x >= 20),
(x < 20), (i == 0), (i != 0),
z++;, x++;, (z > 5)}
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 39/47
Example: generalization of infeasibility arguments
0
1
2
6
Err
z = 0;
x = 0;
(x >= 20)
(z > 5)
true
true
x = 0
false
false
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ ∖ {x++;, (x >= 20)}
(x >= 20)
x++;
Σ
Σ = {z = 0;, x = 0;, (x >= 20),
(x < 20), (i == 0), (i != 0),
z++;, x++;, (z > 5)}
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 40/47
Example: L(P) ⊆ L(R)?
0
1
2
3
4 5
6
Err
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ ∖ {x++;, (x >= 20)}
(x >= 20)
x++;
Σ
L(P) ⊆ L(R) iff the language of
the synchronous product of P
and complemented R is empty.
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 41/47
Example: L(P) ⊆ L(R)?
0
1
2
3
4 5
6
Err
Err
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
true
x = 0
false
Σ ∖ {x = 0;}
x = 0;
Σ ∖ {x++;, (x >= 20)}
(x >= 20)
x++;
Σ
L(P) ⊆ L(R) iff the language of
the synchronous product of P
and complemented R is empty.
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 42/47
Example: the product
0, true
1, true
2, x = 0
3, x = 0
4, x = 0 5, x = 0
6, false
Err, false
2, true
3, true
4, true 5, true
6, true
Err, true
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 43/47
Example: error trace
Err
z1 = 0;
x1 = 0;
(x1 < 20)
(i1 == 0)
x2 = x1 + 1;
(x2 >= 20)
(z1 > 5)
0, true
1, true
2, x = 0
3, x = 0
4, x = 0 5, x = 0
6, false
Err, false
2, true
3, true
4, true 5, true
6, true
Err, true
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 44/47
Example: generalization of infeasibility arguments
Err
true
z1 = 0
z1 = 0
z1 = 0
z1 = 0
z1 = 0
z1 = 0
false
z1 = 0;
x1 = 0;
(x1 < 20)
(i1 == 0)
x2 = x1 + 1;
(x2 >= 20)
(z1 > 5)
0, true
1, true
2, x = 0
3, x = 0
4, x = 0 5, x = 0
6, false
Err, false
2, true
3, true
4, true 5, true
6, true
Err, true
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 45/47
Example: generalization of infeasibility arguments
Err
true
z1 = 0
z1 = 0
z1 = 0
z1 = 0
z1 = 0
z1 = 0
false
true
true
x1 = 0
x1 = 0
x1 = 0
x2 = 1
false
false
z1 = 0;
x1 = 0;
(x1 < 20)
(i1 == 0)
x2 = x1 + 1;
(x2 >= 20)
(z1 > 5)
0, true
1, true
2, x = 0
3, x = 0
4, x = 0 5, x = 0
6, false
Err, false
2, true
3, true
4, true 5, true
6, true
Err, true
z = 0;
x = 0;
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
(x >= 20)
(x < 20)
(i == 0) (i != 0)
z++;
x++;
(z > 5)
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 46/47
Notes
interpolation algorithms exist only for some logics/theories
to handle function calls and unbounded recursion, nested word automata and
nested interpolants are needed
implemented in Ultimate Automizer with numerous optimizations,
e.g. on-the-fly complementation and emptiness check of the product
extensions
for termination analysis: Ultimate Büchi Automizer
for LTL properties: Ultimate LTL Automizer
. . .
Try it out online:
https://www.ultimate-pa.org/
IA159 Formal Methods for Software Analysis: Verification via Automata, Symbolic Execution, and Interpolation 47/47