|Module Name||Formal Verification|
|Module Short Title||Software Verification|
|Semester Taught||Michaelmas Term|
|Contact Hours||Lecture and tutorial hours: 33|
|Module Personnel||Dr. Vasileios Koutavas|
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.
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.
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|
Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition by Michael Huth and Mark Ryan
Lecture notes and handouts.
Assessment in the annual examinations is by written exam (50%) and coursework (50%).
|Academic Year of Data|