Motivation for software verification and formal methods; overview of syntax and semantics and formal proofs in first-order logic; Design by Contract; Hoare logic and program verification; SMT solvers; temporal logic and model checking; brief case studies using selected formal methods.Erasmus/Study abroad studentsIn order to take this module, you should have previously successfully completed an Introduction to Computer Science course and also a Computer Systems course in your ...
Learning Outcomes
Explain the limitations of testing as a means to ensure correctness and evaluate the role of verification in software engineering
Create mathematically precise specifications and designs using logic-based specification languages
Prove the correctness of programs with respect to a specification using Hoare logic
Analyse the properties of formal specifications and designs
Use tools to verify properties of specifications and designs