IA159 Formal Verification Methods
Deductive Software Verification
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
first formal approach to verification of algorithms and
computer programs
partial and total correctness
formal system for verification of flowcharts by Floyd (1967)
axiomatic program verification by Hoare (1969)
Source
Chapter 7 of
D. A. Peled: Software Reliability Methods, Springer, 2001.
IA159 Formal Verification Methods: Deductive Software Verification 2/43
Assumptions and basic terminology
for simplicity we consider only deterministic programs
where the initial values of the program are stored in input
variables x0, x1, . . . and these variables do not change
their values during any execution of the program
a state of a program is an assignment to the program
variables
given a program P and its states a, b, by P(a, b) we denote
the fact that the execution of P starting from the state a
terminates with the state b
a |= ϕ denotes that the state a satisfies the formula ϕ
IA159 Formal Verification Methods: Deductive Software Verification 3/43
Terminology
A specification (or a desired property) of program P is given by
two first order formulae:
initial condition ϕ is a formula with all its free variables
among input variables of P
final assertion ψ
IA159 Formal Verification Methods: Deductive Software Verification 4/43
Two notions of correctness
The program P is
partially correct with respect to ϕ and ψ, written {ϕ}P{ψ}, iff
for all states a, b it holds
P(a, b) ∧ a |= ϕ =⇒ b |= ψ.
If the program starts with a state satisfying ϕ and
then terminates, then the terminal state satisfies ψ.
totally correct with respect to ϕ and ψ, written ϕ P ψ , iff
{ϕ}P{ψ} and for every state a satisfying ϕ the
program terminates.
If the program starts with a state satisfying ϕ, then
it terminates and the terminal state satisfies ψ.
IA159 Formal Verification Methods: Deductive Software Verification 5/43
Formal system for verification of flowcharts
by Robert W Floyd (1936–2001)
1965: associate professor at Carnegie–Mellon University
1968: full professor at Stanford University, without Ph.D.
Floyd–Warshall algorithm: shortest paths in a graph
Floyd–Steinberg dithering: rendering images
program verification, parsing, sorting
IA159 Formal Verification Methods: Deductive Software Verification 6/43
Flowcharts: four kinds of nodes
begin
end
true false
p
v:=e
begin one outgoing edge, no incoming edges
end one incoming edge, no outgoing edges
assignment v := e, where v is a variable, e is a first order term;
one or more incoming edges, one outgoing edge
decision predicate p is an unquantified first order formula;
one or more incoming edges, two outgoing edges
marked with true and false
IA159 Formal Verification Methods: Deductive Software Verification 7/43
Example: what is this program good for?
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
y2:=y2−x2
IA159 Formal Verification Methods: Deductive Software Verification 8/43
Example: what is this program good for?
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
y2:=y2−x2
initial condition
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
final assertion
ψ ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0 ∧ y2 < x2
IA159 Formal Verification Methods: Deductive Software Verification 9/43
Example: what is this program good for?
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
y2:=y2−x2
initial condition
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
final assertion
ψ ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0 ∧ y2 < x2
It computes an integer division.
IA159 Formal Verification Methods: Deductive Software Verification 10/43
Formal system for verification of flowcharts
Proving partial correctness
IA159 Formal Verification Methods: Deductive Software Verification 11/43
Proving partial correctness
A location of a flowchart program is an edge connecting two
flowchart nodes.
To verify that a program P is partially correct with respect to an
initial condition ϕ and a final assertion ψ, it is sufficient to
perform the following two steps.
IA159 Formal Verification Methods: Deductive Software Verification 12/43
Proving partial correctness: step 1
Step 1
to each location of the flowchart we attach a first order
formula called assertion or invariants
to the location exiting from begin we attach ϕ
to the location entering end we attach ψ
Idea
These assertions should be satisfied by every state reachable
in the corresponding location by an execution starting in a state
satisfying ϕ.
IA159 Formal Verification Methods: Deductive Software Verification 13/43
Proving partial correctness: step 2
Given an assignment or decision node c, every assumption on
an incomming edge is called precondition, written pre(c)
an outgoing edge is called postcondition, written post(c)
Idea of step 2
We have to prove that whenever the control of the program is
just before a node c with a state satisfying pre(c) and execution
of c moves the control to the location annotated with post(c),
then the state after the move satisfies post(c).
IA159 Formal Verification Methods: Deductive Software Verification 14/43
Proving partial correctness: step 2
Step 2
Every triple pre(c), c, post(c) is treated according to its form.
1 c is a decision node with a predicate p and post(c) is
associated to the outgoing edge marked with true.
Then we need to prove:
pre(c) ∧ p =⇒ post(c)
2 c is a decision node with a predicate p and post(c) is
associated to the outgoing edge marked with false.
Then we need to prove:
pre(c) ∧ ¬p =⇒ post(c)
IA159 Formal Verification Methods: Deductive Software Verification 15/43
Proving partial correctness: step 2
3 c is an assignment of the form v := e, where v is a
variable and e an expression.
The states before and after the assignment are different
(i.e. pre(c) and post(c) reason about different states).
Therefore, we relativize the postcondition to assert about
the states before the assignment.
Hence, we have to prove
pre(c) =⇒ post(c)[v/e]
where post(c)[v/e] is the assertion post(c) where all
occurences of v are replaced with e.
IA159 Formal Verification Methods: Deductive Software Verification 16/43
Proving partial correctness
proving the consistency between each precondition and
postcondition of all nodes guarantess that {ϕ}P{ψ}
in fact, it guarantees even a stronger property:
In each execution that starts with a state satisfying the
initial condition of the program, when the control of the
program is at some location, the assumption attached to
that location holds.
IA159 Formal Verification Methods: Deductive Software Verification 17/43
Example: partial correctness
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
y2:=y2−x2
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
ψ ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0 ∧ y2 < x2
IA159 Formal Verification Methods: Deductive Software Verification 18/43
Example: partial correctness
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
A
C
FD
E
B
y2:=y2−x2
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
ψ ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0 ∧ y2 < x2
ϕA ≡ ϕ
ϕB ≡ x1 ≥ 0 ∧ x2 > 0 ∧ y1 = 0
ϕC ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0
ϕD ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ x2
ϕE ≡ (x1 = y1 ∗ x2 + y2 − x2) ∧
∧ y2 − x2 ≥ 0
ϕF ≡ ψ
IA159 Formal Verification Methods: Deductive Software Verification 19/43
Example: partial correctness
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
A
C
FD
E
B
y2:=y2−x2
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
ψ ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0 ∧ y2 < x2
ϕA ≡ ϕ
ϕB ≡ x1 ≥ 0 ∧ x2 > 0 ∧ y1 = 0
ϕC ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ 0
ϕD ≡ (x1 = y1 ∗ x2 + y2) ∧
∧ y2 ≥ x2
ϕE ≡ (x1 = y1 ∗ x2 + y2 − x2) ∧
∧ y2 − x2 ≥ 0
ϕF ≡ ψ
Step 2: check the consistency
IA159 Formal Verification Methods: Deductive Software Verification 20/43
Notes
finding assertions for the proof may be a difficult task
there are some heuristics and tools suggesting invariants
there cannot be a fully automatic way of finding them (the
problem is undecidable)
in some programming languages, assertions can be
inserted into the code as additional runtime checks so that
the program will break with a warning message whenever
an invariant is violated
IA159 Formal Verification Methods: Deductive Software Verification 21/43
Programs with array variables: a problem
Example
precondition pre(c) ≡ x[1] = 1 ∧ x[2] = 3
assignment x[x[1]] := 2
postcondition post(c) ≡ x[x[1]] = 2
it is easy to prove
pre(c) =⇒ post(c)[x[x[1]]/2]
as post(c)[x[x[1]]/2] is in fact 2 = 2
but if pre(c) holds and the assignment is performed, then
x[1] = 2 and x[x[1]] = 3 and post(c) does not hold
To handle programs with array variables, the method has to be
modified in one point: relativization of postconditions of
assignment nodes.
IA159 Formal Verification Methods: Deductive Software Verification 22/43
Modification for array variables
let x be an array variable and e1, e2, e3 terms
the syntax of terms is extended with a new construct
(x; e1:e2)[e3], where (x; e1:e2) represents almost the
same array as x, only the element with the index e1 has
been set to e2
to check the consistency of an assignment x[e1] := e2 with
a precondition pre(c) and postcondition post(c), we have
to prove
pre(c) =⇒ post(c)[x/(x; e1:e2)]
the added construct does not increase the expressiveness
of the logic: a formula ρ containing (x; e1:e2)[e3] can be
translated into an equivalent formula
(e1 = e3 ∧ ρ[(x; e1:e2)[e3]/e2]) ∨
∨ (¬(e1 = e3) ∧ ρ[(x; e1:e2)[e3]/x[e3])
IA159 Formal Verification Methods: Deductive Software Verification 23/43
Formal system for verification of flowcharts
Proving termination
IA159 Formal Verification Methods: Deductive Software Verification 24/43
Proving termination: terminology
a partially ordered domain is a pair (W, ) where W is a
set and is a strict partial order relation over W (i.e.
irreflexive, asymmetric, and transitive)
u v has the same meaning as v u
we denote u v when u v or u = v
a well founded domain is a partially ordered domain
containing no infinite sequence of the form
w0 w1 w2 w3 . . .
(i.e. no infinite decreasing sequence)
IA159 Formal Verification Methods: Deductive Software Verification 25/43
Proving termination
To prove the termination with respect to the initial condition ϕ,
we need to do the following steps.
1 We select a well founded domain (W, ) such that W is a
subset of the domain of program variables and is
expressible using the signature of the program.
2 To each location in the flowchart we attach an invariant and
an expression. To the location exiting from begin we
attach ϕ.
3 We show the consistency for each triple pre(c), c, post(c),
as in the partial correctness proof.
IA159 Formal Verification Methods: Deductive Software Verification 26/43
Proving termination
4 We show that whenever an execution starting in a state
satisfying ϕ reaches some location, the value of the
expression associated to this location is within W.
Formally, we prove that for each location with the
associated invariant ρ and expression e it holds:
ρ =⇒ (e ∈ W)
Note that e ∈ W is not, in general, a first order logic
formula. However, it can often be translated into a first
order formula.
IA159 Formal Verification Methods: Deductive Software Verification 27/43
Proving termination
5 We show that in each execution of the program, when
proceeding from a location to its successor location, the
value of the associated expressions does not increase.
Formally, for every node c, an incomming edge with the
associated invariant pre(c) and expression e1, and an
outgoing edge with the associated expression e2
if c is a decision node with a predicate p and e2 is
associated with the true edge, then we prove:
pre(c) ∧ p =⇒ e1 e2
if c is a decision node with a predicate p and e2 is
associated with the false edge, then we prove:
pre(c) ∧ ¬p =⇒ e1 e2
if c is an assignment v := e, then we prove:
pre(c) =⇒ e1 e2[v/e]
IA159 Formal Verification Methods: Deductive Software Verification 28/43
Proving termination
6 In each execution of the program, during a traversal of a
cycle (a loop) in the flowchart there is some point where a
decrease occurs in the value of the associated expressions
from one location to its successor.
Formally, for each cycle we have to find a node with an
incoming and an outgoing edge such that the
corresponding implication above holds even if is
replaced with .
IA159 Formal Verification Methods: Deductive Software Verification 29/43
Example: termination
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
A
C
FD
E
B
y2:=y2−x2
initial condition
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
IA159 Formal Verification Methods: Deductive Software Verification 30/43
Example: termination
begin
true false
end
y1:=0
y2:=x1
y2>=x2
y1:=y1+1
A
C
FD
E
B
y2:=y2−x2
initial condition
ϕ ≡ x1 ≥ 0 ∧ x2 > 0
ϕA ≡ ϕ
ϕB ≡ x1 ≥ 0 ∧ x2 > 0
ϕC ≡ x2 > 0 ∧ y2 ≥ 0
ϕD ≡ x2 > 0 ∧ y2 ≥ x2
ϕE ≡ x2 > 0 ∧ y2 ≥ x2
ϕF ≡ y2 ≥ 0
eA = x1
eB = x1
eC = y2
eD = y2
eE = y2
eF = y2
IA159 Formal Verification Methods: Deductive Software Verification 31/43
Notes
it may be difficult to find the right well founded domain,
invariants, and expressions
termination and partial correctness can be proven
simultaneously.
IA159 Formal Verification Methods: Deductive Software Verification 32/43
Axiomatic program verification
by sir Charles Antony Richard Hoare (1934)
studied in Oxford University and Moscow State University
Quicksort algorithm (1960)
Hoare logic: program verification
Communicating Sequential Processes (CSP)
now in Microsoft Research
IA159 Formal Verification Methods: Deductive Software Verification 33/43
Hoare logic
a proof system that includes both logic and pieces of code
allows to prove different sequential parts of the program
separately (and combine the proofs later)
constructed on top of some first order deduction system
IA159 Formal Verification Methods: Deductive Software Verification 34/43
Hoare logic
contains Hoare triples of the form {ϕ}S{ψ}, where ϕ, ψ are
first order formulae and S is (a part of) a program with the
syntax:
S ::= v := e | skip | S; S | if p then S else S fi |
while p do S end | begin S end
where v is a variable, e is a first order expression, and p is
an unquantified first order formula
a Hoare triple {ϕ}S{ψ} means that if an execution of S
starts with a state satisfying ϕ and S terminates from that
state, then a state satisfying ψ is reached
if S is the entire program, then {ϕ}S{ψ} claims that S is
partially correct with respect to initial condition ϕ and final
assertion ψ
IA159 Formal Verification Methods: Deductive Software Verification 35/43
Axioms and proof rules
Assignment axiom
{ϕ[v/e]}v := e{ϕ}
Skip axiom
{ϕ}skip{ϕ}
Left strengthening rule
ϕ =⇒ ϕ {ϕ }S{ψ}
{ϕ}S{ψ}
Right weakening rule
{ϕ}S{ψ } ψ =⇒ ψ
{ϕ}S{ψ}
IA159 Formal Verification Methods: Deductive Software Verification 36/43
Axioms and proof rules
Sequential composition rule
{ϕ}S1{η} {η}S2{ψ}
{ϕ}S1; S2{ψ}
If-then-else rule
{ϕ ∧ p}S1{ψ} {ϕ ∧ ¬p}S2{ψ}
{ϕ}if p then S1 else S2 fi{ψ}
While rule
{ϕ ∧ p}S{ϕ}
{ϕ}while p do S end{ϕ ∧ ¬p}
Begin-end rule
{ϕ}S{ψ}
{ϕ}begin S end{ψ}
IA159 Formal Verification Methods: Deductive Software Verification 37/43
Derived rules
Assignment axiom + left strengthening rule
ϕ =⇒ ψ[v/e] {ψ[v/e]}v := e{ψ} (axiom)
{ϕ}v := e{ψ}
Sequential composition + right weakening rule
{ψ}S1{η1} η1 =⇒ η2 {η2}S2{ψ}
{ϕ}S1; S2{ψ}
The proof trees are constructed as usual...
IA159 Formal Verification Methods: Deductive Software Verification 38/43
Extensions of Hoare logic
Extensions of the Hoare proof system for verifying concurrent
programs provide axioms for
dealing with shared variables
synchronous and asynchronous communication
procedure calls
They are usually tailored for a particular programming
language, e.g. Pascal or CSP.
IA159 Formal Verification Methods: Deductive Software Verification 39/43
Soundness and completeness
Hoare’s proof system is sound.
It is not complete thanks to incompletenes of first order
logic with natural numbers and basic arithmetic operations
over them (Gödel’s incompletenes theorem).
It is relatively complete, i.e. any correct assertion can be
proved under the following two (sometimes unrealistic)
conditions:
Every correct (first order) logic assertion that is needed in
the proof is already included as an axiom in the proof
system. (Alternatively: there is an oracle (e.g. a human)
deciding whether such an assertion is correct or not.)
Every invariant and intermediate assertion that we need for
the proof can be expressed using the underlying (first
order) logic.
The relative completeness implies that the system is
complete for first order logic with natural numbers with
addition and subtraction as the only operators.
IA159 Formal Verification Methods: Deductive Software Verification 40/43
Notes
Deductive verification
is not limited to finite state systems.
can handle programs of various domains and
datastructures (and even parametrized programs).
can be applied directly to the code (in principle).
can verify that the program is correct (but a bug can occur
in compiler, in hardware, due to a wrong initial condition or
difference between an assumed semantics of code and the
real one, etc.).
is not scalable.
IA159 Formal Verification Methods: Deductive Software Verification 41/43
Notes
In practice, deductive verification
needs a great mental effort as it is mostly manual (the
result depends strongly on the ingenuity of the people
performing verification).
is significantly slower than the typical speed of effective
programming.
is not performed frequently on the actual code.
can be performed on basic algorithms or on abstractions of
the code. The faithfulness of the translation of a program
into an abstracted one can sometimes also be formally
verified.
IA159 Formal Verification Methods: Deductive Software Verification 42/43
Coming next week
Theorem prover ACL2
http://www.cs.utexas.edu/users/moore/acl2/
How it works?
What is it good for?
Including a live show!
IA159 Formal Verification Methods: Deductive Software Verification 43/43