IA159 Formal Verification Methods
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 his slides.
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 2/48
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 3/48
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
z:=0
x:=0
while x<20 {
whif i!=0 then z++
whx++
}
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 4/48
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 5/48
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 6/48
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 7/48
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 in θ occur in both ϕ and ψ,
ϕ =⇒ θ =⇒ ψ.
ϕ ψ
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 8/48
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 in θ occur in both ϕ and ψ,
ϕ =⇒ θ =⇒ ψ.
ϕ ψθ
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 9/48
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 in θ occur in both ϕ and ψ,
ϕ =⇒ θ =⇒ ψ.
ϕ ¬ψ
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 10/48
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 in θ occur in both ϕ and ψ,
ϕ =⇒ θ =⇒ ψ.
ϕ ¬ψθ
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 11/48
Example: program
z:=0
x:=0
while x<20 {
whif i!=0 then z++
whx++
}
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 12/48
Example: error path
z:=0
x:=0
while x<20 {
whif i!=0 then z++
whx++
}
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 13/48
Example: error path
aa 0
1
2
6
Err
z:=0
x:=0
x>=20
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 14/48
Example: feasability analysis
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 15/48
Example: generalization of infeasibility arguments
aa 0
1
2
6
Err
z:=0
x:=0
x>=20
z>5
true
z = 0 ∧ x = 0 ∧
∧ x ≥ 20 ∧ z > 5
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 16/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 17/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 18/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 19/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 20/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 21/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 22/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 23/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 24/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 25/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 26/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 27/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 28/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 29/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 30/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 31/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 32/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 33/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 34/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 35/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 36/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 37/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 38/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 39/48
Example: generalization of infeasibility arguments
aa 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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 40/48
Example: L(P) ⊆ L(R)?
0
1
2
3
4 5
6
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 41/48
Example: L(P) ⊆ L(R)?
0
1
2
3
4 5
6
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 42/48
Example: the product
aa
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 43/48
Example: the product
aa
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 44/48
Example: the product
aa
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 45/48
Example: the product
aa
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 Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 46/48
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://monteverdi.informatik.uni-freiburg.de/tomcat/Website/
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 47/48
Coming next week
Property-Directed Reachability (PDR/IC3)
Another approach based on interpolation.
Very successful in hardware verification (IC3) and popular
in software verification.
IA159 Formal Verification Methods: Verification via Automata, Symbolic Execution, and Interpolation 48/48