Newcastle University School of Computing Science (UK) uses Ada and SPARK for Security and Resilience

Newcastle University School of Computing Science (UK)

Since 2007, students studying for the MSc in Computer Security and Resilience at Newcastle University, UK have been introduced to SPARK Ada to underline the principles of High Integrity Software Development. Ada is not taught exclusively: the course also uses Java in other general programming modules.

SPARK Ada was adopted to give students an understanding, as well as practical experience, of the benefits of a simple, fit-for-purpose language, which allows the ideas of correctness-by-construction, static analysis and automated proof to be explored through the use of an industrial-strength toolset. Students report that the specification-based contract approach is straightforward to understand even without a strong mathematical background, and that they enjoy programming and using the associated examiner and proof tools. Some students go on to conduct their dissertation project using SPARK Ada; even those that do not, benefit from applying the principles to their software engineering practice.

Newcastle University's MSc in Computer Security and Resilience:

http://www.ncl.ac.uk/computing/study/postgrad/taught/5144/