IA159 Formal Methods for Software Analysis
Configurable Program Analysis
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
focus
data-flow analysis (a sort of abstract interpretation, again)
software model checking (= abstract reachability)
configurable program analysis
source
D. Beyer, S. Gulwani, and D. A. Smith: Combining Model Checking and
Data-Flow Analysis, Chapter 16 of Handbook of Model Checking, Springer,
2018.
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 2/56
Motivation
similarity of data-flow analysis and abstract reachability
generalized into configurable program analysis (CPA)
various known algorithms can be seen as CPA instances
CPAs are easy to compose
used in CPAchecker
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 3/56
Control-flow automata
graph representation of functions
nodes = program locations
edges = assumptions and assignments
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 4/56
Control-flow automata
graph representation of functions
nodes = program locations
edges = assumptions and assignments
1 int foo(int y) {
2 int x = 0;
3 int z = 0;
4 if (y == 1) {
5 x = 1;
6 } else {
7 z = 1;
8 }
9 return 10 / (x + z);
10 }
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 5/56
Control-flow automata
Definition (control-flow automaton)
Control-flow automaton (CFA) is a triple (L, l0, G), where
L is a finite set of program locations,
l0 ∈ L is an initial program location, and
G ⊆ L × Ops × L are control-flow edges labeled with operations Ops.
we assume that programs handle only integer variables and contain no
function calls
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 6/56
Semantics of control-flow automata
a concrete state is an assignment c that assigns values to program variables
and also to program counter
C denotes the set of all concrete states
subsets r ⊆ C are called regions
each g = (l, o, l′) ∈ G defines the transition relation
g
→ ⊆ C × {g} × C (this
is the semantics of CFA)
we write c
g
→ c′ instead of (c, g, c′) ∈
g
→
we write c → c′ if c
g
→ c′ for some g ∈ G
c is reachable from a region r if there is a state c′ ∈ r such that c′ →∗
c,
where →∗
denotes the reflexive and transitive closure of →
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 7/56
Semi-lattice
Definition (semi-lattice)
Semi-lattice is a tuple (E, ⊑, ⊔, ⊤), where
(E, ⊑) is a partially ordered set such that each M ⊆ E has the least upper
bound sup(M),
⊔ is the join operator satisfying x ⊔ y = sup({x, y}),
⊤ is the top element ⊤ = sup(E).
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 8/56
Semi-lattice
Definition (semi-lattice)
Semi-lattice is a tuple (E, ⊑, ⊔, ⊤), where
(E, ⊑) is a partially ordered set such that each M ⊆ E has the least upper
bound sup(M),
⊔ is the join operator satisfying x ⊔ y = sup({x, y}),
⊤ is the top element ⊤ = sup(E).
elements of E represent abstract states
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 9/56
Abstract domain
Definition (abstract domain)
Abstract domain is a tuple (C, E, · ), where
C is the set of concrete states,
E = (E, ⊑, ⊔, ⊤) is a semi-lattice,
· : E → 2C is a concretization function.
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 10/56
Abstract domain
Definition (abstract domain)
Abstract domain is a tuple (C, E, · ), where
C is the set of concrete states,
E = (E, ⊑, ⊔, ⊤) is a semi-lattice,
· : E → 2C is a concretization function.
abstract domain determines the aspects of the program that are analyzed
e returns the set of concrete states represented by e
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 11/56
Example
Abstract domain (C, E, · ) for tracking specific values 0, 1 of a variable x
E: ⊤
0 1
⊥
⊤ = C
0 = {c ∈ C | c(x) = 0}
1 = {c ∈ C | c(x) = 1}
⊥ = ∅
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 12/56
Example
Abstract domain (C, E′, · ) for tracking specific values 0, 1 of variables x, z
E′
:
⊥ = ⊥′
⊥′
⊥′
0 ⊥′
1 0⊥′
1⊥′
⊥′
⊤′
00 01 10 11 ⊤′
⊥′
0⊤′
1⊤′
⊤′
0 ⊤′
1
⊤ = ⊤′
⊤′
01 = {c ∈ C | c(x) = 0 ∧ c(z) = 1}
0⊤′ = {c ∈ C | c(x) = 0}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 13/56
Transfer relation
transfer relation
⇝ ⊆ E × G × E represents for each abstract state e its abstract successor e′
under edge g
we write e
g
⇝ e′ instead of (e, g, e′) ∈ ⇝
we write e ⇝ e′ if e
g
⇝ e′ for some g ∈ G
for example, for g with assignment x = z + 1 we have
⊤′
0
g
⇝ 10
01
g
⇝ ⊤′
1
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 14/56
Data-flow analysis
Data-flow analysis (DFA)
may forward abstract interpretation
program locations are now handled explicitly, i.e., we work with pairs (l, e)
instead of l being a part of e
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 16/56
Data-flow analysis (DFA)
may forward abstract interpretation
program locations are now handled explicitly, i.e., we work with pairs (l, e)
instead of l being a part of e
inputs (L, A, ⇝, l0, e0)
program locations L, abstract domain A, transfer relation ⇝
initial abstract state (l0, e0)
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 17/56
Data-flow analysis (DFA)
may forward abstract interpretation
program locations are now handled explicitly, i.e., we work with pairs (l, e)
instead of l being a part of e
inputs (L, A, ⇝, l0, e0)
program locations L, abstract domain A, transfer relation ⇝
initial abstract state (l0, e0)
output
reached : L → E gives a reachable abstract state (l, reached(l)) for each l
reached overapproximates all concrete reachable states, i.e., each concrete
state c reachable from (l0, e0) is in l∈L (l, reached(l))
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 18/56
Data-flow analysis (DFA)
1 algorithm DFA(L, A, ⇝, l0, e0)
2 waitList ← {l0}
3 reached(l0) ← e0
4 while waitList ̸= ∅ do
5 choose l from waitList
6 waitList ← waitList ∖ {l}
7 foreach (l′
, e′
) such that (l, reached(l)) ⇝ (l′
, e′
) do
8 if e′
̸⊑ reached(l′
) then
9 reached(l′
) ← reached(l′
) ⊔ e′
10 waitList ← waitList ∪ {l′
}
11 return reached
if reached(l′) has not been defined yet, then
e′
̸⊑ reached(l′
) is true
reached(l′
) ⊔ e′
evaluates to e′
the algorithm finishes if the height of the semi-lattice in A is finite
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 19/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 20/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
waitList = {2}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 21/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
waitList = {3}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 22/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
waitList = {4}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 23/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
reached(5) = 00 reached(7) = 00
waitList = {5, 7}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 24/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
reached(5) = 00 reached(7) = 00
reached(9) = 10
waitList = {7, 9}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 25/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
reached(5) = 00 reached(7) = 00
reached(9) =
10 ⊔ 01 = ⊤′
⊤′
waitList = {9}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 26/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
reached(5) = 00 reached(7) = 00
reached(9) =
10 ⊔ 01 = ⊤′
⊤′
reached(10) = ⊤′
⊤′
waitList = {10}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 27/56
Example
Track the values 0, 1 of variables x, z using the data-flow analysis with the abstract
domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached(2) = ⊤′
⊤′
reached(3) = 0⊤′
reached(4) = 00
reached(5) = 00 reached(7) = 00
reached(9) =
10 ⊔ 01 = ⊤′
⊤′
reached(10) = ⊤′
⊤′
waitList = ∅
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 28/56
Software model checking
Software model checking
computes all reachable abstract states according to the transfer relation
join operator is never applied
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 30/56
Software model checking
computes all reachable abstract states according to the transfer relation
join operator is never applied
inputs (L, A, ⇝, l0, e0)
program locations L, abstract domain A, transfer relation ⇝
initial abstract state (l0, e0)
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 31/56
Software model checking
computes all reachable abstract states according to the transfer relation
join operator is never applied
inputs (L, A, ⇝, l0, e0)
program locations L, abstract domain A, transfer relation ⇝
initial abstract state (l0, e0)
output
reached ⊆ L × E of reachable abstract states
reached overapproximates all concrete reachable states, i.e., each concrete
state c reachable from (l0, e0) is in (l,e)∈reached (l, e)
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 32/56
Software model checking
1 algorithm Reach(L, A, ⇝, l0, e0)
2 waitList ← {(l0, e0)}
3 reached ← {(l0, e0)}
4 while waitList ̸= ∅ do
5 choose (l, e) from waitList
6 waitList ← waitList ∖ {(l, e)}
7 foreach (l′
, e′
) such that (l, e) ⇝ (l′
, e′
) do
8 if there is no (l′
, e′′
) ∈ reached such that e′
⊑ e′′
then
9 reached ← reached ∪ {(l′
, e′
)}
10 waitList ← waitList ∪ {(l′
, e′
)}
11 return reached
finishes if the semi-lattice is finite
there are infinite semi-lattices of a finite height
typically slower, but more precise than data-flow analysis
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 33/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 34/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
waitList = {(2, ⊤′
⊤′
)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 35/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
waitList = {(3, 0⊤′
)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 36/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
(4, 00),
waitList = {(4, 00)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 37/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
waitList = {(5, 00), (7, 00)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 38/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
waitList = {(7, 00), (9, 10)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 39/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
(9, 01),
waitList = {(9, 10), (9, 01)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 40/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
}
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
(9, 01),
(10, 10),
waitList = {(9, 01), (10, 10)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 41/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
(9, 01),
(10, 10),
(10, 01)}
waitList = {(10, 10), (10, 01)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 42/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
(9, 01),
(10, 10),
(10, 01)}
waitList = {(10, 01)}
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 43/56
Example
Track the values 0, 1 of variables x, z using software model checking with the
abstract domain based on the semi-lattice E′ and the initial abstract state (2, ⊤′⊤′).
2
3
4
5 7
9
10
x = 0;
z = 0;
(y == 1) !(y == 1)
x = 1; z = 1;
ret = 10 / (x + z);
reached = { (2, ⊤′
⊤′
),
(3, 0⊤′
),
(4, 00),
(5, 00),
(7, 00),
(9, 10),
(9, 01),
(10, 10),
(10, 01)}
waitList = ∅
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 44/56
Configurable program analysis
Similarity of the two algorithms
1 algorithm DFA(L, A, ⇝, l0, e0)
2 waitList ← {l0}
3 reached(l0) ← e0
4 while waitList ̸= ∅ do
5 choose l from waitList
6 waitList ← waitList ∖ {l}
7 foreach (l′
, e′
) such that (l, reached(l)) ⇝ (l′
, e′
) do
8 if e′
̸⊑ reached(l′
) then
9 reached(l′
) ← reached(l′
) ⊔ e′
10 waitList ← waitList ∪ {l′
}
11 return reached
1 algorithm Reach(L, A, ⇝, l0, e0)
2 waitList ← {(l0, e0)}
3 reached ← {(l0, e0)}
4 while waitList ̸= ∅ do
5 choose (l, e) from waitList
6 waitList ← waitList ∖ {(l, e)}
7 foreach (l′
, e′
) such that (l, e) ⇝ (l′
, e′
) do
8 if there is no (l′
, e′′
) ∈ reached such that e′
⊑ e′′
then
9 reached ← reached ∪ {(l′
, e′
)}
10 waitList ← waitList ∪ {(l′
, e′
)}
11 return reached
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 46/56
Configurable program analysis
Definition (configurable program analysis)
Configurable program analysis (CPA) is a tuple (A, ⇝, merge, stop), where
A is an abstract domain,
⇝ is a transfer relation,
merge : E × E → E is a merge operator that combines two abstract states
such that it can weaken the second abstract state based on the first one
(correspond to widening), i.e., e′ ⊑ merge(e, e′) ⊑ ⊤,
stop : E × 2E → B is a termination check such that stop(e, R) checks if e is
covered (in some sense) by the set of abstract states R.
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 47/56
Configurable program analysis
unifies the data-flow analysis and software model checking
handles program locations implicitly
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 48/56
Configurable program analysis
unifies the data-flow analysis and software model checking
handles program locations implicitly
inputs (A, ⇝, merge, stop, e0)
CPA (A, ⇝, merge, stop)
initial abstract state e0
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 49/56
Configurable program analysis
unifies the data-flow analysis and software model checking
handles program locations implicitly
inputs (A, ⇝, merge, stop, e0)
CPA (A, ⇝, merge, stop)
initial abstract state e0
output
reached ⊆ E of reachable abstract states
reached overapproximates all concrete reachable states, i.e., each concrete
state c reachable from e0 is in e∈reached e
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 50/56
Configurable program analysis
1 algorithm CPA(A, ⇝, merge, stop, e0)
2 waitList ← {e0}
3 reached ← {e0}
4 while waitList ̸= ∅ do
5 choose e from waitList
6 waitList ← waitList ∖ {e}
7 foreach e′
such that e ⇝ e′
do
8 foreach e′′
∈ reached do
9 enew = merge(e′
, e′′
)
10 if enew ̸= e′′
then
11 waitList ← (waitList ∪ {enew }) ∖ {e′′
}
12 reached ← (reached ∪ {enew }) ∖ {e′′
}
13 if ¬stop(e′
, reached) then
14 waitList ← waitList ∪ {e′
}
15 reached ← reached ∪ {e′
}
16 return reached
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 51/56
Notes
typical instances of merge
mergesep(e, e′) = e′
mergejoin(e, e′) = e ⊔ e′
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 52/56
Notes
typical instances of merge
mergesep(e, e′) = e′
mergejoin(e, e′) = e ⊔ e′
typical instances of stop
stopsep
(e, R) = (∃e′ ∈ R.e ⊑ e′)
stopjoin
(e, R) = e ⊑ e′∈R e′
another parameter of all the algorithms is the order in which elements of
waitList are processed
for example, it can correspond to depth-first search or breadth-first search
different strategies are used in practice
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 53/56
Notes
there are CPA instances for
reachable-code analysis
constant propagation
reaching definitions
predicate analysis
observer automata
value analysis
symbolic execution
. . .
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 54/56
Notes
a CPA can be constructed as a combination of simpler CPAs (easier to
implement)
combinations used in practice
constant propagation + predicate analysis + (strengthening)
predicate analysis + observer automata
. . .
can be extended with the notion of precision and CEGAR
can be used for computation of program invariants
implemented in CPAchecker
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 55/56
Notes
a CPA can be constructed as a combination of simpler CPAs (easier to
implement)
combinations used in practice
constant propagation + predicate analysis + (strengthening)
predicate analysis + observer automata
. . .
can be extended with the notion of precision and CEGAR
can be used for computation of program invariants
implemented in CPAchecker
CPAchecker
verification tool developed by the group of Dirk Beyer since 2007
implements various techniques, supports their combinations
available under the Apache 2.0 License
https://cpachecker.sosy-lab.org/
IA159 Formal Methods for Software Analysis: Configurable Program Analysis 56/56