1. Review Sites
  2. Home
  3. Modules
  4. Verification

Module: Verification

Program verification techniques, Hoare’s axiomatic approach.

Learning Outcomes

Perform elementary program verification.

Readings

Rosen Ch. 1 (Logic and Proofs) and 5 (Induction and Recursion)

Sections 1.1, 1.6, 5.5: Program verification techniques, 5.5: Hoare’s axiomatic approach

Textbook 32 pages

Program verification, part 1

Applications of predicate logic, program verification, program assertions, axioms and inference rules.

Lecture notes

Program verification, part 2

Examples of verification of straightline programs, verification of sequential programs with loops

Lecture notes

Experiential Learning

Program correctness

Prove program segment properties (Rosen Section 5.5)

Problems

Program correctness

Prove program segment properties (Rosen Section 5.5)

Solutions