Formal Verification of Programs

Péter Battyányi

University of Debrecen

Made within the framework of the project TÁMOP-4.1.2.A/1-11/1-2011-0103.

New Széchenyi Plan logo

Hungary’s renewal logo


Table of Contents

1. While programs
The operational semantics of while programs
Denotational semantics of while programs
Partial correctness of while-programs
The stepwise Floyd–Naur method
Hoare logic from a semantical point of view
Proof outlines
Proof rules for the Hoare calculus
The wlp-calculus
Relative completeness of the Hoare partial correctness calculus
The wp-calculus
Total correctness
Soundness of the Hoare total correctness calculus
Relative completeness of the Hoare total correctness calculus
2. Recursive programs
Proving partial correctness for recursive procedures
Total correctness of recursive procedures
3. Disjoint parallel programs
4. Shared variable parallelism
The syntax of shared variable parallel programs
Operational semantics
Deduction system
Soundness and completeness
Case study
5. Synchronization
Proof rules for partial correctness
Mutual exclusion
A. Mathematical background
Sets and relations
Complete partial orders and fixpoint theorems
B. Exercises
Operational semantics
Denotational semantics
Partial correctness in Hoare logic
Total correctness of while programs
The wp-calculus
Recursive programs