Description: Formal methods for the validation/verification of safety critical software, including machine learning algorithms. Topics covered will include mathematical modelling for embedded, automation, and mechatronic systems; advanced techniques for validation and verification; techniques for formal specification; methods of verification such as Bisimulation and model checking; state space explosion problem and solutions such as BDDs, symbolic model checking, and modular verification; verification of HDL/C using model checking tools. Includes a significant individual research project.