Skip to main content

Trinity College Dublin, The University of Dublin

Menu Search

Module DescriptorSchool of Computer Science and Statistics

Module CodeCS4004
Module NameFormal Verification
Module Short TitleSoftware Verification
Semester TaughtMichaelmas Term
Contact HoursLecture and tutorial hours: 33
Module PersonnelDr. Vasileios Koutavas
Learning Outcomes

Having successfully completed this module, students will:

  • Have gained signidicant knowledge of mathematical logics (propositional and first order logic) and the Floyd/Hoare logic for program specification. These logics are the basis for software verification, and are the de facto standard in the verification industry.
  • Understand the current state-of-the-art in software verification technology, its range of applicability and theoretical limitations, and the necessary programmer input required to overcome these limitations.
  • Be able to use logic formulas to specify the correct behaviour of programs, including programs implementing well-known algorithms (e.g. binary search), new programs provided to them, and programs they write themselves to solve engineering problems.
  • Learn to use the state-of-the-art in software verification tools (e.g. Microsoft Dafny) to mechanically verify program correctness in a team setting.
    Learn how to use pencil-and-paper mathematical proofs to manually verify program correctness.
  • Understand the impact of software faults in different areas of engineering, such as aerospace and medical, and how this translates to financial, ethical, and human well-being.
Learning Aims

Increasingly complex computer systems are becoming ever more important in all aspects of our lives. There are numerous examples where software bugs had extremely serious consequences, financially or to human well-being. This module will explore techniques to mathmatiically verify that computer systems satisfy their specifications; i.e., that they have no bugs and are thus safe to use. The focus will be mainly on software correctness.

These techniques rely on precise mathematical logics and proof systems appropriate for software verification. State-of-the-art tools will be used to verify the correctness of programs.

Module Content

Specification languages and logics; axiomatic program semantics. Formal proof systems to verify software and system properties such as propositional, predicate and Hoare logic. Proofs by mathematical, structural, and rule induction. Correcness proofs of functional and imperative programs.

Recommended Reading List

Main textbook:
Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition by Michael Huth and Mark Ryan

Lecture notes and handouts.

Module Prerequisites
Assessment Details

Assessment in the annual examinations is by written exam (50%) and coursework (50%).

Module Website
Academic Year of Data