Module Descriptor School of Computer Science and Statistics
|Module Name||Formal Verification|
|Module Short Title||Software Verification|
|Semester Taught||Michaelmas Term|
Lecture and tutorial hours: 33
|Module Personnel||Dr. Vasileios Koutavas|
Having successfully completed this module, students will:
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.
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|
Assessment in the annual examinations is by written exam (65%) and coursework (35%). Assessment in the supplementals is by 100% written examination only
|Academic Year of Data||2017/18|