IA169 System Verification and Assurance
Deductive Verification
Jiří Barnat
Verification of Algorithms
Validation and Verification
A general goal of V&V is to prove correct behaviour of
algorithms.
Reminder
Testing is incomplete.
Testing can detect errors but cannot prove correctness.
Conclusion
Need for another different way of verification.
IA169 System Verification and Assurance – 04 str. 2/30
Formal Verification
Goal of formal Verification
The goal is to show that system behaves correctly with the
same level of confidence as it is given with a mathematical
proof.
Requirements
Formally precise semantics of system behaviour.
Formally precise definition of system properties to be shown.
Methods of formal verification
Deductive verification
Model checking
Abstract interpretation
IA169 System Verification and Assurance – 04 str. 3/30
Section
Deductive verification
IA169 System Verification and Assurance – 04 str. 4/30
Notion of Correctness
Program is correct if
it terminates for a valid input and returns correct output.
There is a need to show two parts – partial correctness and
termination.
Partial correctness (Correctness, Soundness)
If the computation terminates for valid input values (i.e.
values for which the program is defined) the resulting values
are correct.
Termination (Completness, Convergence)
If executed on valid input values, the computation always
terminates.
IA169 System Verification and Assurance – 04 str. 5/30
Verification of Serial Programs
Serial programs (sequential)
Input-output-closed and finite programs.
All input values are known prior program execution.
All output values are stored in output variables.
Examples: Quick sort, Greater common divider, . . .
General Principle
Program instructions are viewed as state transformers.
The goal is to show that the mutual relation of input and
output values is as expected or given by the specification.
I.e. to verify the correctness of procedure of transformation of
input values to output values.
IA169 System Verification and Assurance – 04 str. 6/30
Expressing Program Properties
State of Computation
State of computation of a program is given by the value of
program counter and values of all variables.
Atomic predicates
Basic statements about individual states of the computation.
The validity is deduced purely from the values of variables
given by the state of computation.
Examples of atomic propositions: (x == 0), (x1 >= y3).
Beware of the scope of variables.
Set of States
Can be described with a Boolean combination of atomic
predicates.
Example: (x == m) ∧ (y > 0)
IA169 System Verification and Assurance – 04 str. 7/30
Expressing Program Properties – Assertions
Assertion
For a given program location defines a Boolean expression
that should be satisfied with the current values of program
variables in the given location.
Invariant of a program location.
Assertions – Proving Correctness
Assigning properties to individual locations of Control Flow
Graph.
Robert Floyd: Assigning Meanings to Programs (1967)
IA169 System Verification and Assurance – 04 str. 8/30
Error Detection — Assertion Violation
Testing
Assertion violation serves as a test oracle.
Run-Time Checking
Checking location invariants during run-time.
Improved error localisation as the assertion violated relates to
a particular program line.
Undetected Errors
If the error does not exhibit for given input data.
If the program behaves non-deterministically (parallelism).
IA169 System Verification and Assurance – 04 str. 9/30
Section
Hoare Proof System
IA169 System Verification and Assurance – 04 str. 10/30
Hoare Proof System
Principle
Programs = State Transformers.
Specification = Relation between input and output state of
computation.
Hoare logic
Designed for showing partial correctness of programs.
Let P and Q be predicates and S be a program, then
{P} S {Q}
is the so called Hoare triple.
Intended meaning of {P} S {Q}
S is a program that transforms any state satisfying
pre-condition P to a state satisfying post-condition Q.
IA169 System Verification and Assurance – 04 str. 11/30
Pre- and Post- Conditions
Example
{z = 5} x = z ∗ 2 {x > 0}
Valid triple, though post-condition could be more precise
(stronger).
Example of a stronger post-condition: {x > 5 ∧ x < 20}.
Obviously, {x > 5 ∧ x < 20} =⇒ {x > 0}.
The Weakest Pre-Condition
P is the weakest pre-condition, if and only if
{P}S{Q} is a valid triple and
∀P such that {P }S{Q} is valid, P =⇒ P.
Edsger W. Dijkstra (1975)
IA169 System Verification and Assurance – 04 str. 12/30
Proving in Hoare System
How to prove {P} S {Q}
Pick suitable conditions P’ a Q’
Decomposition into three sub-problems:
{P’} S {Q’} P =⇒ P’ Q’ =⇒ Q
Use axioms and rules of Hoare system to prove {P’} S {Q’}.
P =⇒ P’ and Q’ =⇒ Q are called proof obligations.
Proof obligations are proven in the standard way.
IA169 System Verification and Assurance – 04 str. 13/30
Hoare System – Axiom for Assignment
Axiom
Assignment axiom: {φ[x replaced with k]} x := k {φ}
Meaning
Triple {P}x := y{Q} is an axiom in Hoare system, if it holds
that P is equal to Q in which all occurrences of x has been
replaced with y.
Examples
{y+7>42} x:=y+7 {x>42} is an axiom
{r=2} r:=r+1 {r=3} is not an axiom
{r+1=3} r:=r+1 {r=3} is an axiom
IA169 System Verification and Assurance – 04 str. 14/30
Hoare Logic – Example 1
Example
Prove that the following program returns value greater than
zero if executed for value of 5.
Program: out := in ∗ 2
Proof
1) We built a Hoare triple:
{in = 5} out := in ∗ 2 {out > 0}
2) We deduce/guess a suitable pre-condition:
{in ∗ 2 > 0}
3) We prove Hoare triple:
{in ∗ 2 > 0} out := in ∗ 2 {out > 0} (axiom)
4) We prove auxiliary statement:
(in = 5) =⇒ (in ∗ 2 > 0)
IA169 System Verification and Assurance – 04 str. 15/30
Hoare System – Example of a Rule
Rule
Sequential composition: {φ}S1{χ}∧{χ}S2{ψ}
{φ}S1;S2{ψ}
Meaning
If S1 transforms a state satisfying φ to a state satisfying χ
and S2 transforms a state satisfying χ to a state satisfying ψ
then the sequence S1; S2 transforms a state satisfying φ to a
state satisfying ψ.
In the proof
Should {φ}S1; S2{ψ} be used in the proof, an intermediate
condition χ has to be found, and {φ}S1{χ} and {χ}S2{ψ}
have to be proven.
IA169 System Verification and Assurance – 04 str. 16/30
Hoare System – Partial Correctness
Axiom for skip: {φ} skip {φ}
Axiom for :=: {φ[x := k]}x:=k{φ}
Composition rule: {φ}S1{χ}∧{χ}S2{ψ}
{φ}S1;S2{ψ}
Conditional rule: {φ∧B}S1{ψ}∧{φ∧¬B}S2{ψ}
{φ}if B then S1 else S2 fi{ψ}
While rule: {φ∧B}S{φ}
{φ}while B do S od {φ∧¬B}
Consequence rule: φ =⇒ φ ,{φ }S{ψ },ψ =⇒ ψ
{φ}S{ψ}
IA169 System Verification and Assurance – 04 str. 17/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{
r = 1;
while (n= 0) {
r = r * n;
n = n - 1;
} {
Notes:
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{ n ≥ 0 ∧ t=n } {P}
r = 1;
while (n= 0) {
r = r * n;
n = n - 1;
}
{ r=t! } {Q}
Notes:
Reformulation in terms of Hoare logic.
Note the use of auxiliary variable t.
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{ n ≥ 0 ∧ t=n } {P}
r = 1;
{ n ≥ 0 ∧ t=n ∧ r = 1 } {I1}
while (n= 0) {
r = r * n;
n = n - 1;
}
{ r=t! } {Q}
Notes:
{n ≥ 0 ∧ t=n ∧ 1=1} r=1 { n ≥ 0 ∧ t=n ∧ r=1 }
(n ≥ 0 ∧ t=n) =⇒ (n ≥ 0 ∧ t=n ∧ 1=1)
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{ n ≥ 0 ∧ t=n } {P}
r = 1;
{ n ≥ 0 ∧ t=n ∧ r = 1 } {I1}
while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2}
r = r * n;
n = n - 1;
}
{ r=t! } {Q}
Notes:
Invariant of a cycle: {I2} ≡ { r=t!/n! ∧ t ≥ n ≥ 0 }
I1 =⇒ I2 ( I2 ∧ ¬(n=0) ) =⇒ Q
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{ n ≥ 0 ∧ t=n } {P}
r = 1;
{ n ≥ 0 ∧ t=n ∧ r = 1 } {I1}
while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2}
r = r * n;
{ r=t!/(n-1)! ∧ t ≥ n > 0 } {I3}
n = n - 1;
}
{ r=t! } {Q}
Notes:
{ r*n = t!/(n-1)! ∧ t ≥ n > 0 } r=r*n {I3}
I2 ∧ (n=0) =⇒ ( r*n = t!/(n-1)! ∧ t ≥ n > 0 )
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic – Example 2
Prove that for n ≥ 0 the following code computes n!.
{ n ≥ 0 ∧ t=n } {P}
r = 1;
{ n ≥ 0 ∧ t=n ∧ r = 1 } {I1}
while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2}
r = r * n;
{ r=t!/(n-1)! ∧ t ≥ n > 0 } {I3}
n = n - 1;
}
{ r=t! } {Q}
Notes:
{ r = t!/(n-1)! ∧ t ≥ (n-1) ≥ 0 } n=n-1 {I2}
I3 =⇒ ( r = t!/(n-1)! ∧ t ≥ (n-1) ≥ 0 )
IA169 System Verification and Assurance – 04 str. 18/30
Hoare Logic and Completness
Observation
Hoare logic allowed us to reduce the problem of proving
program correctness to a problem of proving a set of
mathematical statements with arithmetic operations.
Notice about correctness’s and (in)completeness
Hoare logic is correct, i.e. if it is possible to deduce {P}S{Q}
then executing program S from a state satisfying P may
terminate only in a state satisfying Q.
If a proof system is strong enough to express integral
arithmetics, it is necessarily incomplete, i.e. there exists claims
that cannot be proven or dis-proven using the system.
Hoare system for proving correctness of programs is
incomplete due to the proof obligations generated with the
consequence rule.
IA169 System Verification and Assurance – 04 str. 19/30
Hoare Logic and Proving Correctness in Practice
Troubles with Proof Construction
Often pre- and post- condition must be suitable reformulated
for the purpose of the proof.
It is very difficult to identify loop invariants.
Partial Correctness in Practice
Often reduced to formulation of all the loop invariants, and
demonstration that they actually are the loop invariants.
The proof of being an invariant is often achieved with math
induction.
IA169 System Verification and Assurance – 04 str. 20/30
Proving Termination
Well-Founded Domain
Partially ordered set that does not contain infinitely
decreasing sequence of members.
Examples: (N,<), (PowerSet(N),⊆)
Proving Termination
For every loop in the program a suitable well-founded domain
and an expression over the domain is chosen.
It is shown that the value associated with a location cannot
grow along any instruction that is part of the loop.
It is shown that there exists at least one instruction in the
loop that decreases the value of the expression.
IA169 System Verification and Assurance – 04 str. 21/30
Section
Automating Deductive Verification
IA169 System Verification and Assurance – 04 str. 22/30
Principles of Automation of Deductive Verification
Pre-processing
Transformation of program to a suitable intermediate
language.
Examples of IL: Boogie (Microsoft Research), Why3 (INRIA)
Structural Analysis and Construction of the Proof Skeleton
Identification of Hoare triples, loop invariants and suitable
pre- and post-conditions (some of that might be given with
the program to be verified).
Generation of auxiliary proof obligations.
Solving proof obligations
Using tools for automated proving.
May be human-assisted.
IA169 System Verification and Assurance – 04 str. 23/30
Solving Proof Obligations
Tools for Automated Proving
User guides a tool to construct a proof.
HOL, ACL2, Isabelle, PVS, Coq, ...
Reduced to the satisfiability problem
Employ SAT and SMT solvers.
Z3, ...
IA169 System Verification and Assurance – 04 str. 24/30
Automated Proving
Proof
A finite sequence of steps that using axioms and rules of a
given proof system that transforms assumptions ψ into the
conclusion ϕ.
Observation
For systems with finitely many axioms and rules, proofs may
be systematically generated. Hence, for all provable claims the
proof can be found in finite time.
All reasonable proving systems has infinitely many axioms.
Consider, e.g. an axiom x = x. This is virtually a shortcut
(template) for axioms 1 = 1, 2 = 2, 3 = 3, etc.
Semi-decidable with dove-tailing approach.
IA169 System Verification and Assurance – 04 str. 25/30
Automated Proofing
Searching for a Proof of Valid Statement
The number of possible finite sequences of steps of rules and
axiom applications is too many (infinitely many).
In general there is no algorithm to find a proof in a given
proof system even for a valid statement.
Without some clever strategy, it cannot be expected that a
tool for automated proof generation will succeed in a
reasonable short time.
The strategy is typically given by an experienced user of the
automated proving tool. The user typically has to have
appropriate mathematical feeling and education.
At the end, the tool is used as a mechanical checker for a
human constructed proof.
IA169 System Verification and Assurance – 04 str. 26/30
Verification with Tools for Automated Proofing
Theorem Provery
The goal is find the proof within a given proof system.
the proof is searched for in two modes:
Algorithmic mode – Application of rules and axioms
Guided by the user of the tool.
Application of the general proving techniques, such as
deduction, resolution, unification, . . . .
Search mode – Looking for new valid statements
Employs brute-force approach and various heuristics.
Existing Tools
The description of system (axioms, rules) as well as the claim
to be proven is given in the language of the tool.
IA169 System Verification and Assurance – 04 str. 27/30
Results of Proof Searching
Possible Outputs
a) Proof has been found and checked.
b) Proof has not been found.
The statement is valid, can be proven, but the proof has not
yet been found.
The statement is valid, but it cannot be proven in the system.
The statement is invalid.
Observation
In the case that no proof has been found, there is no
indication of why it is so.
IA169 System Verification and Assurance – 04 str. 28/30
Dafny
http://rise4fun.com/dafny
IA169 System Verification and Assurance – 04 str. 29/30
Practicals and Homework – 04
Practicals
Dafny (rise4fun.com)
http://www.doc.ic.ac.uk/~scd/Dafny_Material/
Exercises_%20Arithm_Terms_Loops.docx
Homework
Prove correctness of the following program using Dafny
method Count(N: nat, M: int, P: int) returns (R: int) {
var a := M;
var b := P;
var i := 1;
while (i <= N) {
a := a+3;
b := 2*a+b+1;
i := i+1;
}
R := b;
}
Read and repeat: Jaco van de Pol: Automated verification
of Nested DFS
IA169 System Verification and Assurance – 04 str. 30/30