Skip to main content

Formal Verification

Module code: CSU55004 · Semester: Semester 1

Questions by Year​

0 of 7 done · tick papers and add notes as you go

Papers open on tcd.ie (sign in to TCD first).

Topics

  • Propositional logic LO1
  • First-order (predicate) logic LO1
  • Hoare logic and axiomatic semantics LO1, LO3
  • Proof by induction; correctness of functional and imperative programs LO5
  • Mechanical verification with Dafny LO2, LO4, LO6
Learning outcomes (exam covers LO1–5)
  1. Know propositional, first-order and Hoare logic for specification
  2. Understand the state of the art in verification and its limits
  3. Write logic specifications of program behaviour
  4. Verify software mechanically with tools such as Dafny, in a team
  5. Write manual correctness proofs
  6. Design programs that can be verified

Summarised from the module descriptor, checked November 2026.