IA159 Formal Verification Methods
Abstraction
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
Focus
principle of abstraction
exact abstractions and non-exact abstractions
predicate abstraction
CEGAR: counterexample-guided abstraction refinement
Sources
Chapter 13 of E. M. Clarke, O. Grumberg, and D. A. Peled:
Model Checking, MIT, 1999.
R. Pelánek: Reduction and Abstraction Techniques for
Model Checking, PhD thesis, FI MU, 2006.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith:
Counterexample-guided Abstraction Refinement for
Symbolic Model Checking, J. ACM 50(5), 2003.
IA159 Formal Verification Methods: Abstraction 2/94
Motivation
Abstraction is probably the most important technique
for reducing the state explosion problem.
[CGP99]
Original
system
oo Verification impossible
// Properties
IA159 Formal Verification Methods: Abstraction 3/94
Motivation
Abstraction is probably the most important technique
for reducing the state explosion problem.
[CGP99]
Original
system
oo // Abstract
model
oo Verification // Properties
IA159 Formal Verification Methods: Abstraction 4/94
Motivation
Abstraction is probably the most important technique
for reducing the state explosion problem.
[CGP99]
Original
system
oo // Abstract
model
oo Verification // Properties
large finite systems −→ smaller finite systems
infinite-state systems −→ finite systems
IA159 Formal Verification Methods: Abstraction 5/94
Intuition

x = 0

x = 3
??
x = 1

x = 2
__
IA159 Formal Verification Methods: Abstraction 6/94
Intuition

x = 0

x = 3
??
x = 1

x = 2
__
IA159 Formal Verification Methods: Abstraction 7/94
Intuition

x = 0

x = 3
??
x = 1

x = 2
__

x = 0


x > 0
MM
MM
IA159 Formal Verification Methods: Abstraction 8/94
Intuition

x = 0

x = 3
??
x = 1

x = 2
__

x = 0


x > 0
MM
MM
equivalent with respect to F(x > 0)
nonequivalent with respect to GF(x = 0)
IA159 Formal Verification Methods: Abstraction 9/94
Simulation
Given two Kripke structures M = (S, →, S0, L) and
M = (S , → , S0, L ), we say that M simulates M, written
M ≤ M , if there exists a relation R ⊆ S × S such that:
∀s0 ∈ S0 . ∃s0 ∈ S0 : (s0, s0) ∈ R
(s, s ) ∈ R =⇒ L(s) = L (s )
(s, s ) ∈ R ∧ s → p =⇒ ∃p ∈ S : s → p ∧ (p, p ) ∈ R
IA159 Formal Verification Methods: Abstraction 10/94
Simulation
Given two Kripke structures M = (S, →, S0, L) and
M = (S , → , S0, L ), we say that M simulates M, written
M ≤ M , if there exists a relation R ⊆ S × S such that:
∀s0 ∈ S0 . ∃s0 ∈ S0 : (s0, s0) ∈ R
(s, s ) ∈ R =⇒ L(s) = L (s )
(s, s ) ∈ R ∧ s → p =⇒ ∃p ∈ S : s → p ∧ (p, p ) ∈ R
Lemma
If M ≤ M , then for every path σ = s1s2 . . . of M starting in an
initial state there is a run σ = s1s2 . . . of M starting in an initial
state and satisfying
L(s1)L(s2) . . . = L (s1)L (s2) . . . .
IA159 Formal Verification Methods: Abstraction 11/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 12/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 13/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 14/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
???
hh
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 15/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
???
hh
If A has a behaviour violating ϕ (i.e. A |= ϕ), then either
1 M has this behaviour as well (i.e. M |= ϕ), or
2 M does not have this behaviour, which is then called
false positive or spurious counterexample
(M |= ϕ or M |= ϕ due to another behaviour violating ϕ).
IA159 Formal Verification Methods: Abstraction 16/94
Relations between original and abstract systems
Original
system
M
oo M ≥ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 17/94
Relations between original and abstract systems
Original
system
M
oo M ≥ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 18/94
Relations between original and abstract systems
Original
system
M
oo M ≥ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 19/94
Relations between original and abstract systems
Original
system
M
oo M ≥ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 20/94
Relations between original and abstract systems
Original
system
M
oo M ≥ A //
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
???
hh
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA159 Formal Verification Methods: Abstraction 21/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
Note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐=
IA159 Formal Verification Methods: Abstraction 22/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
Note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐=
IA159 Formal Verification Methods: Abstraction 23/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
Note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐=
IA159 Formal Verification Methods: Abstraction 24/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
Note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐=
IA159 Formal Verification Methods: Abstraction 25/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
Note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐=
IA159 Formal Verification Methods: Abstraction 26/94
Relations between original and abstract systems
Original
system
M
oo M ≤ A
M ≥ A
//
Abstract
model
A
oo
A |= ϕ
// Property
ϕ ∈ LTL66
M |= ϕ
hh
All these relations hold even for ϕ ∈ CTL∗
.
IA159 Formal Verification Methods: Abstraction 27/94
Abstraction
Exact abstractions
IA159 Formal Verification Methods: Abstraction 28/94
Cone of influence (aka dead variables)
Idea
We eliminate the variables that do not influence the variables in
the specification.
IA159 Formal Verification Methods: Abstraction 29/94
Cone of influence (aka dead variables)
let V be the set of variables appearing in specification
cone of influence C of V is the minimal set of variables
such that
V ⊆ C
if v occurs in a test affecting the control flow, then v ∈ C
if there is an assignment v := e for some v ∈ C, then all
variables occurring in the expression e are also in C
C can be computed by the source code analysis
variables that are not in C can be eliminated from the code
together with all commands they participate in
IA159 Formal Verification Methods: Abstraction 30/94
Cone of influence: example
S: v := getinput();
x := getinput();
y := 1;
z := 1;
while v > 0 do
z := z ∗ x;
x := x − 1;
y := y ∗ v;
v := v − 1;
z := z ∗ y;
E:
Specification: F(pc = E)
IA159 Formal Verification Methods: Abstraction 31/94
Cone of influence: example
S: v := getinput();
x := getinput();
y := 1;
z := 1;
while v > 0 do
z := z ∗ x;
x := x − 1;
y := y ∗ v;
v := v − 1;
z := z ∗ y;
E:
Specification: F(pc = E)
V = ∅, C = {v}
IA159 Formal Verification Methods: Abstraction 32/94
Cone of influence: example
S: v := getinput(); S: v := getinput();
x := getinput(); skip;
y := 1; skip;
z := 1; skip;
while v > 0 do while v > 0 do
z := z ∗ x; skip;
x := x − 1; skip;
y := y ∗ v; skip;
v := v − 1; v := v − 1;
z := z ∗ y; skip;
E: E:
Specification: F(pc = E)
V = ∅, C = {v}
IA159 Formal Verification Methods: Abstraction 33/94
Other exact abstractions
Symmetry reduction
in systems with more identical parallel components, their
order is not important
Equivalent values
if the set of behaviours starting in a state s is the same for
values a, b of a variable v, then the two values can be
replaced by one
applicable to larger sets of values as well
used in timed automata for timer values
IA159 Formal Verification Methods: Abstraction 34/94
Abstraction
Non-exact abstractions
IA159 Formal Verification Methods: Abstraction 35/94
Concept
We face two problems
1 to find a suitable a set of abstract states and a mapping
between the original states and the abstract ones
2 to compute a transition relation on abstract states
IA159 Formal Verification Methods: Abstraction 36/94
Finding abstract states
Abstract states are usually defined in one of the following ways:
1 for each variable x, we replace the original variable domain
Dx by an abstract domain Ax and we define a total function
hx : Dx → Ax
a state s = (v1, . . . , vm) ∈ Dx1
× . . . × Dxm given by values
of all variables corresponds to an abstract state
h(s) = (hx1
(v1), . . . , hxm (vm)) ∈ Ax1
× . . . × Axm
2 predicate abstraction - we choose a finite set
Φ = {φ1, . . . , φn} of predicates over the set of variables;
we have several choices of abstract domains
The first approach can be seen as a special case the latter one.
IA159 Formal Verification Methods: Abstraction 37/94
Popular abstract domains for integers
Sign abstraction
Ax = {a+, a−, a0}
hx (v) =



a− if v < 0
a0 if v = 0
a+ if v > 0
Parity abstraction
Ax = {ae, ao}
hx (v) =
ae if v is even
ao if v is odd
good for verification of properties related to the last bit of
binary representation
IA159 Formal Verification Methods: Abstraction 38/94
Popular abstract domains for integers
Congruence modulo an integer
hx (v) = v (mod m) for some m
nice properties:
((x mod m) + (y mod m)) mod m = x + y (mod m)
((x mod m) − (y mod m)) mod m = x − y (mod m)
((x mod m) · (y mod m)) mod m = x · y (mod m)
Representation by logarithm
hx (v) = log2(v + 1)
the number of bits needed for representation of v
good for verification of properties related to overflow
problems
IA159 Formal Verification Methods: Abstraction 39/94
Popular abstract domains for integers
Single bit abstraction
Ax = {0, 1}
hx (v) =the i-th bit of v for a fixed i
Single value abstraction
Ax = {0, 1}
hx (v) =
1 if v = c
0 otherwise
...and others
IA159 Formal Verification Methods: Abstraction 40/94
Predicate abstraction
Let Φ = {φ1, . . . , φn} be a set of predicates over the set of
variables.
Abstract domain {0, 1}n
a state s = (v1, . . . , vm) corresponds to an abstract state
given by a vector of truth values of {φ1, . . . , φn}, i.e.
h(s) = (φ1(v1, . . . , vm), . . . , φn(v1, . . . , vm)) ∈ {0, 1}n
example: φ1 = (x1 > 3) φ2 = (x1 < x2) φ3 = (x2 > 10)
s = (5, 7)
h(s) = (1, 1, 0)
IA159 Formal Verification Methods: Abstraction 41/94
Abstract structures
Assume that
we have a Kripke structure M = (S, →, S0, L)
we have an abstract domain A and a mapping h : S → A
To define abstract model (A, → , A0, LA), we set
A0 = {h(s0) | s0 ∈ S0}
LA : A → 2AP has be correctly defined, i.e.
for abstraction based on variable domains, validity of atomic
propositions is determined by abstract states in Ax1
×...×Axm
for predicate abstraction, validity of atomic propositions is
determined by abstraction predicates {φ1, . . . , φn} (AP is
typically a subset of it)
and LA has to agree with L, i.e. L(s) = LA(h(s))
IA159 Formal Verification Methods: Abstraction 42/94
Abstract structures
Assume that
we have a Kripke structure M = (S, →, S0, L)
we have an abstract domain A and a mapping h : S → A
We define two abstract models:
Mmay = (A, →may , A0, LA), where
a1 →may a2 iff there exist s1, s2 ∈ S such that
h(s1) = a1, h(s2) = a2, and s1 → s2
IA159 Formal Verification Methods: Abstraction 43/94
Example Mmay
x=0EE
// x=1 //
aa x=2 //
aa x=3 //
xx
x=4 //
xx
x=5 //
· · ·
xx
. . .
Mmay with abstract domain {0, 1}2 generated by predicate
abstraction with predicates φ1 = (x > 0) and φ2 = (x > 2).
IA159 Formal Verification Methods: Abstraction 44/94
Example Mmay
x=0EE
// x=1 //
aa x=2 //
aa x=3 //
xx
x=4 //
xx
x=5 //
· · ·
xx
. . .
Mmay with abstract domain {0, 1}2 generated by predicate
abstraction with predicates φ1 = (x > 0) and φ2 = (x > 2).
(0, 0)
HH
// (1, 0)
VV
//
ff
(1, 1)
VV
vv
IA159 Formal Verification Methods: Abstraction 45/94
Abstract structures
Assume that
we have a Kripke structure M = (S, →, S0, L)
we have an abstract domain A and a mapping h : S → A
We define two abstract models:
Mmust = (A, →must , A0, LA), where
a1 →must a2 iff for each s1 ∈ S satisfying h(s1) = a1
there exists s2 ∈ S such that h(s2) = a2
and s1 → s2
IA159 Formal Verification Methods: Abstraction 46/94
Example Mmust
x=0EE
// x=1 //
aa x=2 //
aa x=3 //
xx
x=4 //
xx
x=5 //
· · ·
xx
. . .
Mmust with abstract domain {0, 1}2 generated by predicate
abstraction with predicates φ1 = (x > 0) and φ2 = (x > 2).
IA159 Formal Verification Methods: Abstraction 47/94
Example Mmust
x=0EE
// x=1 //
aa x=2 //
aa x=3 //
xx
x=4 //
xx
x=5 //
· · ·
xx
. . .
Mmust with abstract domain {0, 1}2 generated by predicate
abstraction with predicates φ1 = (x > 0) and φ2 = (x > 2).
(0, 0)
HH
// (1, 0)
ff
(1, 1)
VV
vv
IA159 Formal Verification Methods: Abstraction 48/94
Relations between M, Mmust, and Mmay
Lemma
For every Kripke structure M, abstract domain A with a
mapping function h it holds:
Mmust ≤ M ≤ Mmay
IA159 Formal Verification Methods: Abstraction 49/94
Relations between M, Mmust, and Mmay
Lemma
For every Kripke structure M, abstract domain A with a
mapping function h it holds:
Mmust ≤ M ≤ Mmay
computing Mmust or Mmay requires constructing M first
(recall that M can be very large or even infinite)
we rather compute an under-approximation Mmust of Mmust
or an over-approximation Mmay of Mmay directly from the
implicit representation of M
it holds that Mmust ≤ Mmust ≤ M ≤ Mmay ≤ Mmay
IA159 Formal Verification Methods: Abstraction 50/94
Abstraction
Abstraction in practice
IA159 Formal Verification Methods: Abstraction 51/94
Predicate abstraction: abstracting sets of states
Abstract domain {0, 1}n is not used in practice (too many
transitions) =⇒ it is better to assign a single abstract state to a
set of original states.
Abstract domain 2{0,1}n
let b = b1, . . . , bn be a vector of bi ∈ {0, 1}
we set [b, Φ] = b1 · φ1 ∧ . . . ∧ bn · φn,
where 0 · φi = ¬φi and 1 · φi = φi
let X denotes the set of original states
h(X) = {b ∈ {0, 1}n | ∃s ∈ X : s |= [b, Φ]}
example: φ1 = (x1 > 3) φ2 = (x1 < x2) φ3 = (x2 > 10)
X = {(5, 7), (4, 5), (2, 9)}
h(X) = {(1, 1, 0), (0, 1, 0)}
nice theoretical properties
not used in practice (this abstract domain grows too fast)
IA159 Formal Verification Methods: Abstraction 52/94
Predicate abstraction: abstracting sets of states
Abstract domain {0, 1, ∗}n (predicate-cartesian abstraction)
let b = b1, . . . , bn be a vector of bi ∈ {0, 1, ∗}
we set [b, Φ] = b1 · φ1 ∧ . . . ∧ bn · φn,
where 0 · φi = ¬φi, 1 · φi = φi, and ∗ · φi =
h(X) = min{b ∈ {0, 1, ∗}n | ∀s ∈ X : s |= [b, Φ]},
where min means “the most specific”
example: φ1 = (x1 > 3) φ2 = (x1 < x2) φ3 = (x2 > 10)
X = {(5, 7), (4, 5), (2, 9)}
h(X) = (∗, 1, 0)
this one is used in practice
IA159 Formal Verification Methods: Abstraction 53/94
Guarded command language
Syntax
let V be a finite set of integer variables
expressions over V use standard binary operations
(+, −, ·, . . .) and boolean relations (=, <, >)
Act is a set of action names
model is a pair M = (V, E), where E = {t1, . . . , tm} is a
finite set of transitions of the form ti = (ai, gi, ui), where
ai ∈ Act
gi is a boolean expression over V
ui is a sequence of assignments over V
IA159 Formal Verification Methods: Abstraction 54/94
Guarded command language
Syntax
let V be a finite set of integer variables
expressions over V use standard binary operations
(+, −, ·, . . .) and boolean relations (=, <, >)
Act is a set of action names
model is a pair M = (V, E), where E = {t1, . . . , tm} is a
finite set of transitions of the form ti = (ai, gi, ui), where
ai ∈ Act
gi is a boolean expression over V
ui is a sequence of assignments over V
Semantics
M defines a labelled transition system where
states are valuations of variables S = 2V→Z
initial state is the zero valuation s0(v) = 0 for all v ∈ V
s
ai
→ s whenever s |= gi and s = ui (s)
IA159 Formal Verification Methods: Abstraction 55/94
Example
x=0
b
EE
a // x=1
a //
c
aa x=2
a //
c
aa x=3
a //
d
xx
x=4
a //
d
xx
x=5
a //
d · · ·
xx
. . .
implicit description in guarded command language:
V = {x}
(a, , x := x + 1)
(b, ¬(x > 0), x := 0)
(c, (x > 0) ∧ (x ≤ 2), x := 0)
(d, (x > 2), x := 0)
IA159 Formal Verification Methods: Abstraction 56/94
Abstraction in practice
we use predicate abstraction with domain {0, 1, ∗}n
given a formula ϕ with free variables from V, we set
pre(ai, ϕ) = (gi =⇒ ϕ[x/ui(x)])
we use a sound decision procedure is_valid, i.e.
is_valid(ϕ) = =⇒ ϕ is a tautology
(the procedure is_valid does not have to be complete)
IA159 Formal Verification Methods: Abstraction 57/94
Abstraction in practice
for every abstract state b ∈ {0, 1, ∗}n and for every transition
ti = (ai, gi, ui), we compute an over-approximation of a
may-successor of b under ti as
if is_valid([b, Φ] =⇒ ¬gi) then there is no successor
otherwise, the successor b is given by
bj =



1 if is_valid([b, Φ] =⇒ pre(ai, φj))
0 if is_valid([b, Φ] =⇒ pre(ai, ¬φj))
∗ otherwise
IA159 Formal Verification Methods: Abstraction 58/94
Example
bj =



1 if is_valid([b, Φ] =⇒ pre(ai, φj))
0 if is_valid([b, Φ] =⇒ pre(ai, ¬φj))
∗ otherwise
(a, , x := x + 1)
using the predicates φ1 = (x > 0), φ2 = (x > 2), we compute
the transition
(1, 0)
a
→may (1, ∗)
IA159 Formal Verification Methods: Abstraction 59/94
Example
bj =



1 if is_valid([b, Φ] =⇒ pre(ai, φj))
0 if is_valid([b, Φ] =⇒ pre(ai, ¬φj))
∗ otherwise
(a, , x := x + 1)
using the predicates φ1 = (x > 0), φ2 = (x > 2), we compute
the transition
(1, 0)
a
→may (1, ∗)
(x > 0) ∧ (x ≤ 2) =⇒ ( =⇒ (x + 1 > 0)) is true
IA159 Formal Verification Methods: Abstraction 60/94
Example
bj =



1 if is_valid([b, Φ] =⇒ pre(ai, φj))
0 if is_valid([b, Φ] =⇒ pre(ai, ¬φj))
∗ otherwise
(a, , x := x + 1)
using the predicates φ1 = (x > 0), φ2 = (x > 2), we compute
the transition
(1, 0)
a
→may (1, ∗)
(x > 0) ∧ (x ≤ 2) =⇒ ( =⇒ (x + 1 > 0)) is true
(x > 0) ∧ (x ≤ 2) =⇒ ( =⇒ (x + 1 > 2)) is not true
(x > 0) ∧ (x ≤ 2) =⇒ ( =⇒ (x + 1 ≤ 2)) is not true
IA159 Formal Verification Methods: Abstraction 61/94
Abstraction in practice
for every transition, we compute successors of all abstract
states
based on the successors, we transform the original implicit
representation of a system into a boolean program
boolean program is an implicit representation of an
over-approximation of Mmay
it uses only boolean variables b representing the validity of
abstraction predicates Φ
boolean program can be used as an input for a suitable
model checker (of finite-state systems)
IA159 Formal Verification Methods: Abstraction 62/94
Example
V = {x}
(a, , x := x + 1)
(b, ¬(x > 0), x := 0)
(c, (x > 0) ∧ (x ≤ 2), x := 0)
(d, (x > 2), x := 0)
using the predicates φ1 = (x > 0), φ2 = (x > 2), we get the
boolean program (defining an over-approximation) of Mmay
V = {b1, b2}, where b1, b2 represents validity of φ1, φ2
(a, , b1 := if b1 then 1 else ∗
b2 := if b2 then 1 else if b1 then ∗ else 0)
(b, ¬b1, b1 := 0, b2 := 0)
(c, b1 ∧ ¬b2, b1 := 0, b2 := 0)
(d, b2, b1 := 0, b2 := 0)
IA159 Formal Verification Methods: Abstraction 63/94
Example of a real NQC code and its absraction
task light_sensor_control() { task A_light_sensor_control() {
int x = 0; bool b = false;
while (true) { while (true) {
if (LIGHT > LIGHT_THRESHOLD) { if (*) {
PlaySound(SOUND_CLICK);
Wait(30);
x = x + 1; b = b ? true : * ;
} else { } else {
if (x > 2) { if (b) {
PlaySound(SOUND_UP);
ClearTimer(0);
brick = LONG; brick = LONG;
} else if (x > 0) { } else if (b ? true : *) {
PlaySound(SOUND_DOUBLE_BEEP);
ClearTimer(0);
brick = SHORT; brick = SHORT;
} }
x = 0; b = false;
} }
} }
} }
IA159 Formal Verification Methods: Abstraction 64/94
Abstraction
CEGAR: counterexample-guided abstraction refinement
IA159 Formal Verification Methods: Abstraction 65/94
Motivation
it is hard to find a small and valuable abstraction
abstraction predicates are usually provided by a user
CEGAR tries to find a suitable abstraction automatically
implemented in SLAM, BLAST, Static Driver Verifier (SDV),
and many others
incomplete method, but very successfull in practice
IA159 Formal Verification Methods: Abstraction 66/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 67/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 68/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 69/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 70/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 71/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 72/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 73/94
Principle
system M
((
specification ϕ
AP(ϕ)vv

build a new
abstract model
M (M ≤ M )

add new
abstraction
predicates
22
model check
M |= ϕ?
NO
ss YES

analyze
counterexamplespurious
VV
real

BUG!
M |= ϕ
NO BUG!
M |= ϕ
IA159 Formal Verification Methods: Abstraction 74/94
Notes
added abstraction predicates ensure that the new abstract
model M does not have the behaviour corresponding to
the spurious counterexample of the previous M
the analysis of an abstract counterexample and finding
new abstract predicates are nontrivial tasks
the method is sound but incomplete
(the algorithm can run in the cycle forever)
IA159 Formal Verification Methods: Abstraction 75/94
Counterexample analysis
Case 1 Finite path counterexample (e.g. for reachability)
S := h−1(a1) ∩ Init
j := 1
while S = ∅ ∧ j < n
j := j + 1
S := S
S := Succ(S) ∩ h−1(aj)
if S = ∅ then return real bug
else return j, S //spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA159 Formal Verification Methods: Abstraction 76/94
Counterexample analysis
Case 1 Finite path counterexample (e.g. for reachability)
S := h−1(a1) ∩ Init
j := 1
while S = ∅ ∧ j < n
j := j + 1
S := S
S := Succ(S) ∩ h−1(aj)
if S = ∅ then return real bug
else return j, S //spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA159 Formal Verification Methods: Abstraction 77/94
Counterexample analysis
Case 1 Finite path counterexample (e.g. for reachability)
S := h−1(a1) ∩ Init
j := 1
while S = ∅ ∧ j < n
j := j + 1
S := S
S := Succ(S) ∩ h−1(aj)
if S = ∅ then return real bug
else return j, S //spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA159 Formal Verification Methods: Abstraction 78/94
Counterexample analysis
Case 1 Finite path counterexample (e.g. for reachability)
S := h−1(a1) ∩ Init
j := 1
while S = ∅ ∧ j < n
j := j + 1
S := S
S := Succ(S) ∩ h−1(aj)
if S = ∅ then return real bug
else return j, S //spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
output: j = 4, S = {s9}
we need a predicate separating {s9} and {s7} to remove
this spurious counterexample
IA159 Formal Verification Methods: Abstraction 79/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 80/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 81/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 82/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 83/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 84/94
Counterexample analysis
Case 2 Lasso counterexample
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
an abstract loop may correspond to loops of different size
and starting at different stages of the unwinding
the unwinding eventually becomes periodic, the size of the
period is the least common multiple of the size of individual
loops
IA159 Formal Verification Methods: Abstraction 85/94
Counterexample analysis
Analysis of a lasso counterexample can be reduced to analysis
of a finite path counterexample.
Theorem
Abstract lasso a1 . . . ai(ai+1 . . . an)ω corresponds to a concrete
lasso iff there is a concrete path corresponding to the abstract
path a1 . . . ai(ai+1 . . . an)m+1, where m = mini+1≤j≤n |h−1(aj)|.
IA159 Formal Verification Methods: Abstraction 86/94
Counterexample analysis
Analysis of a lasso counterexample can be reduced to analysis
of a finite path counterexample.
Theorem
Abstract lasso a1 . . . ai(ai+1 . . . an)ω corresponds to a concrete
lasso iff there is a concrete path corresponding to the abstract
path a1 . . . ai(ai+1 . . . an)m+1, where m = mini+1≤j≤n |h−1(aj)|.
a1 a2 a3
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 87/94
Counterexample analysis
Analysis of a lasso counterexample can be reduced to analysis
of a finite path counterexample.
Theorem
Abstract lasso a1 . . . ai(ai+1 . . . an)ω corresponds to a concrete
lasso iff there is a concrete path corresponding to the abstract
path a1 . . . ai(ai+1 . . . an)m+1, where m = mini+1≤j≤n |h−1(aj)|.
a1 a2 a3
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA159 Formal Verification Methods: Abstraction 88/94
Abstraction refinement
. . .
. . . ai−1 ai ai+1 . . .
. . .
Si−1
SB
SI
SD
SB = h−1(ai) ∩ Succ−1
(h−1(ai+1)) bad states
SI = h−1(ai) (SB ∪ SD) irrelevant states
SD = Si dead-end states
IA159 Formal Verification Methods: Abstraction 89/94
Abstraction refinement
. . .
. . . ai−1 ai ai+1 . . .
. . .
Si−1
SB
SI
SD
SB = h−1(ai) ∩ Succ−1
(h−1(ai+1)) bad states
SI = h−1(ai) (SB ∪ SD) irrelevant states
SD = Si dead-end states
To eliminate the spurious counterexample, we need to refine
the abstraction such that no abstract state simultaneously
contains states from SB and from SD.
IA159 Formal Verification Methods: Abstraction 90/94
Abstraction refinement
Consider abstract state (3≤x≤5) ∧ (7≤y≤9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
IA159 Formal Verification Methods: Abstraction 91/94
Abstraction refinement
Consider abstract state (3≤x≤5) ∧ (7≤y≤9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
−→
3 4 5
7 B + I I
8 D + I B
9 D + I D
or
3 4 5
7
B + I D + I
9
8 D B + I
?
there could be more possible abstraction refinements
we want the coarsest refinement (i.e. with the least number
of abstract states)
IA159 Formal Verification Methods: Abstraction 92/94
Abstraction refinement
Consider abstract state (3≤x≤5) ∧ (7≤y≤9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
−→
3 4 5
7 B + I I
8 D + I B
9 D + I D
or
3 4 5
7
B + I D + I
9
8 D B + I
?
there could be more possible abstraction refinements
we want the coarsest refinement (i.e. with the least number
of abstract states)
Theorem
The problem of finding the coarsest refinement is NP-hard.
−→ heuristics
IA159 Formal Verification Methods: Abstraction 93/94
Coming next week
Abstract interpretation + static analysis
Another standard approach.
Applicable to large software projects, e.g. Linux kernel.
What can one learn about a program without executing it?
IA159 Formal Verification Methods: Abstraction 94/94