IA159 Formal Verification Methods
Property Directed Reachability
(PDR/IC3)
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
Focus
representation of a finite system by boolean formulas
property directed reachability
Source
N. Een, A. Mishchenko, and R. Brayton: Efficient
Implementation of Property Directed Reachability, FMCAD
2011.
Special thanks to Marek Chalupa for providing me his slides.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 2/27
Short history of IC3/PDR
IC3
the tool introduced in 2010
(3rd place in Hardware Model Checking Competition 2010)
abbreviation for Incremental Construction of Inductive
Clauses for Indubitable Correctness
described in A. R. Bradley: SAT-Based Model Checking
Without Unrolling, VMCAI 2011.
PDR
name for the technique implemented in IC3
abbreviation for Property Directed Reachability
suggested by N. Een, A. Mishchenko, and R. Brayton
they also simplified and improved the algorithm
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 3/27
Short history of IC3/PDR
originally formulated for finite systems where states are
valuations of boolean variables: good for HW, not for SW
later generalized for other kinds of systems, in particular
for program verification
combined with predicate abstraction, k-induction, . . .
IC3/PDR is currently considered to be one of the most powerfull
verification techniques.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 4/27
Important papers about IC3/PDR
K. Hoder and N. Bjorner: Generalized Property Directed
Reachability, SAT 2012.
A. Cimatti, A. Griggio: Software Model Checking via IC3,
CAV 2012.
A. R. Bradley: Understanding IC3, SAT 2012.
T. Welp, A. Kuehlmann: QF_BV Model Checking with
Property Directed Reachability, DATE 2013.
A. Cimatti, A. Griggio, S. Mover, S. Tonetta: IC3 Modulo
Theories via Implicit Predicate Abstraction, TACAS 2014.
J. Birgmeier, A. R. Bradley, G. Weissenbacher:
Counterexample to
Induction-Guided-Abstraction-Refinement (CTIGAR), CAV
2014.
D. Jovanovi´c, B. Dutertre: Property-Directed k-Induction,
FMCAD 2016.
A. Gurfinkel, A. Ivrii: K-Induction without Unrolling, FMCAD
2017.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 5/27
Formalization of the problem
Finite state machine
set of state variables ¯x = {x1, x2, . . . , xn}
states are valuations v : ¯x → {0, 1}
initial states given by a propositional formula I over ¯x
transition relation given by a propositional formula T over
¯x ∪ ¯x , where ¯x = {x1, . . . , xn} describe the target states
Property
given by a propositional formula P over ¯x
The problem
To decide whether all reachable states of a given finite state
machine (¯x, I, T) satisfy a given property P.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 6/27
Example
00 01 10 11
¯x = {x1, x2}
I = ¬x1 ∧ ¬x2
T = (¬x1 ∧ ¬x2 ∧ ¬x1 ∧ ¬x2) ∨ (¬x1 ∧ x2 ∧ ¬x1 ∧ x2) ∨
(¬x1 ∧ x2 ∧ x1 ∧ ¬x2) ∨ (x1 ∧ x1 ∧ x2)
= (x1 ∨ x2 ∨ ¬x1) ∧ (x1 ∨ x2 ∨ ¬x2) ∧
(x1 ∨ ¬x2 ∨ x2 ∨ x1) ∧ (x1 ∨ ¬x2 ∨ ¬x1 ∨ ¬x2) ∧
(¬x1 ∨ x2 ∨ x1) ∧ (¬x1 ∨ x2 ∨ x2) ∧
(¬x1 ∨ ¬x2 ∨ x1) ∧ (¬x1 ∨ ¬x2 ∨ x2)
P = ¬x1 ∨ ¬x2
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 7/27
Terminology and notation
for any formula F over ¯x, F denotes the same formula
over ¯x
cube is a conjunction of literals
clause is a disjunction of literals
negation of a cube is a clause (and vice versa)
a cube with all variables of ¯x represents at most one state
a set of clauses R = {c1, . . . , ck } is interpreted as
conjunction c1 ∧ . . . ∧ ck
each formula can be identified with a set of states
(and vice versa)
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 8/27
Intuition
A set S of states is inductive invariant if S ∧ T =⇒ S .
We are looking for an inductive invariant S satisfying
I =⇒ S (i.e. S contains all reachable states) and
S =⇒ P (i.e. all states of S satisfy the property).
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 9/27
Intuition
A set S of states is inductive invariant if S ∧ T =⇒ S .
We are looking for an inductive invariant S satisfying
I =⇒ S (i.e. S contains all reachable states) and
S =⇒ P (i.e. all states of S satisfy the property).
I
reachable
states
S
P
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 10/27
Intuition
A set S of states is inductive invariant if S ∧ T =⇒ S .
We are looking for an inductive invariant S satisfying
I =⇒ S (i.e. S contains all reachable states) and
S =⇒ P (i.e. all states of S satisfy the property).
I
reachable
states
S
P
Note that P does not have to be an inductive invariant.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 11/27
Traces
The algorithm gradually builds traces, which are sequences
R0, R1, . . . , RN of formulas called frames such that
R0 = I and for all i < N
Ri =⇒ Ri+1
Ri ∧ T =⇒ Ri+1
Ri =⇒ P
R0=IR1R2R2P · · ·
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 12/27
Traces
The algorithm gradually builds traces, which are sequences
R0, R1, . . . , RN of formulas called frames such that
R0 = I and for all i < N
Ri =⇒ Ri+1
Ri ∧ T =⇒ Ri+1
Ri =⇒ P
R0=IR1R2R2P · · ·
Intuitively, each Ri represents a superset of states reachable
from initial states in at most i steps.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 13/27
Traces
The algorithm gradually builds traces, which are sequences
R0, R1, . . . , RN of formulas called frames such that
R0 = I and for all i < N
Ri =⇒ Ri+1
Ri ∧ T =⇒ Ri+1
Ri =⇒ P
R0=IR1R2R2P · · ·
Intuitively, each Ri represents a superset of states reachable
from initial states in at most i steps.
Moreover, for each i > 0 it holds that
Ri is a set of clauses
Ri+1 ⊆ Ri (which implies Ri =⇒ Ri+1)
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 14/27
Proof-obligations
let R0, . . . , RN be a trace where RN =⇒ P does not hold
let s be a state satisfying RN ∧ ¬P
we want to prove that s is not reachable in N steps
so called proof-obligation (s, N)
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 15/27
Solving proof-obligation (s, k)
1 check satisfiability of Rk−1 ∧ T ∧ s
2 if unsatisfiable, then
Rk−1 is strong enough to block s
thus we can add the clause ¬s to Rk
we add it also to all R1, . . . , Rk−1 to keep Ri+1 ⊆ Ri valid
proof-obligation solved
3 if satisfiable, then
s has some immediate predecessor t in Rk−1
if k − 1 = 0 then return property violated and
extract counterexample from proof-obligations
if k − 1 > 0 then solve proof-obligation (t, k − 1) and go to 1
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 16/27
Proof-obligations
IR1R2
...RN−2RN−1RN
P
s
Proof-obligations
IR1R2
...RN−2RN−1RN
P
s t
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 18/27
PDR: high level view
1 if I ∧ ¬P is satisfiable then return property violated
2 R0 := I
3 N := 0
4 while RN ∧ ¬P is satisfiable do
find a state s satisfying RN ∧ ¬P
solve proof-obligation (s, N)
5 RN+1 := ∅
6 N := N + 1
7 propagate learned clauses
for each i from 1 to N − 1
for each clause c ∈ Ri , if Ri ∧ T =⇒ c then add c to Ri+1
8 if Ri = Ri+1 for some i then return property satisfied
(Ri is inductive invariant)
9 go to 4
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 19/27
Termination
Termination follows from finiteness of considered systems
each proof-obligation must be solved in finitely many steps
(either successfully or by detection of proterty violation)
if the shortest path to a state violating P has j steps, then
some state violating P is discovered when N = j
if P is satisfied, an inductive invariant is eventually found as
there are only finitely many sets of states
R0, R1, . . . , RN always represent sets ordered by inclusion
if Ri and Ri+1 become semantically equivalent, then clause
propagation makes them also syntactically equivalent
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 20/27
Termination
Termination follows from finiteness of considered systems
each proof-obligation must be solved in finitely many steps
(either successfully or by detection of proterty violation)
if the shortest path to a state violating P has j steps, then
some state violating P is discovered when N = j
if P is satisfied, an inductive invariant is eventually found as
there are only finitely many sets of states
R0, R1, . . . , RN always represent sets ordered by inclusion
if Ri and Ri+1 become semantically equivalent, then clause
propagation makes them also syntactically equivalent
Still, for a system with ¯x = {x1, . . . , xn}, we may need a trace
with up to 2n elements to find an inductive invariant.
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 21/27
PDR: important tricks
The presented algorithm is correct, but slow.
PDR uses several tricks to boost efficiency, in particular it
generalizes blocked states
uses relative induction in proof-obligation solving
blocks states in future frames
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 22/27
Generalization of blocked states
the presented proof-obligation algorithm adds ¬s to Rk
when s is blocked, i.e. Rk−1 ∧ T ∧ s is unsatisfiable
PDR generalizes this state to a set of states that are
blocked for the same reason
there are several ways to achieve that
use ternary simulation
use unsat cores
use interpolants
manually drop parts of s
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 23/27
Generalization of blocked states
the presented proof-obligation algorithm adds ¬s to Rk
when s is blocked, i.e. Rk−1 ∧ T ∧ s is unsatisfiable
PDR generalizes this state to a set of states that are
blocked for the same reason
there are several ways to achieve that
use ternary simulation
use unsat cores
use interpolants
manually drop parts of s
Use of unsat cores
one can build the cube r of the literals of s that appear in
the unsat core and then add ¬r to Rk
the clause ¬r is smaller than ¬s and represents less states
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 24/27
Relative induction in proof-obligation solving
to solve proof-obligation (s, k), we checked Rk−1 ∧ T ∧ s
PDR checks satisfiability of Rk−1 ∧ ¬s ∧ T ∧ s instead
this query is more likely to be unsatisfied (it has one more
clause) and state s can be blocked sooner
in fact, it checks whether ¬s is inductive relative to Rk−1:
the query is unsatisfiable iff (Rk−1 ∧ ¬s ∧ T) =⇒ ¬s
intuitively, in this way we ignore self-loops of the system
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 25/27
Relative induction in proof-obligation solving
to solve proof-obligation (s, k), we checked Rk−1 ∧ T ∧ s
PDR checks satisfiability of Rk−1 ∧ ¬s ∧ T ∧ s instead
this query is more likely to be unsatisfied (it has one more
clause) and state s can be blocked sooner
in fact, it checks whether ¬s is inductive relative to Rk−1:
the query is unsatisfiable iff (Rk−1 ∧ ¬s ∧ T) =⇒ ¬s
intuitively, in this way we ignore self-loops of the system
in fact, PDR combines this technique with the
generalization of blocked clauses
thus, PDR searches for a subclause (ideally minimal)
c ⊆ ¬s such that I =⇒ c and (Rk−1 ∧ c ∧ T) =⇒ c
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 26/27
The End
Thank you for your attention!
individual oral exam via a videocall (approx 30 min)
open-book exam, what matters is your understanding
every student gets one randomly selected topic to explain
overview of formal methods
reachability in pushdown systems
partial order reduction
. . .
IA159 Formal Verification Methods: Property Directed Reachability, (PDR/IC3) 27/27