View Proposal

Proposer
Andrew Ireland
Title
Dafny: A Programming and Verification Language
Goal
Develop teaching materials for the Dafny programming and verification language.
Description
Dafny supports the development of safe and secure software. Dafny is both a programming language and verification environment. As a programming language, Dafny shares the features that are common to most imperative programming languages. So why learn a new language? Well once you have developed your provably correct programs in Dafny they can be automatically translated into a range of other languages, i.e., C#, Java, JavaScript, Go and Python (with more to come). Through an in-depth study, the aim of this project is to develop teaching materials that provide an introduction to the Dafny programming and verification language that highlights both its strengths and limitations.
Resources
https://dafny.org/
Background
Ideally F20RS
Url
External Link
Difficulty Level
Challenging
Ethical Approval
None
Number Of Students
1
Supervisor
Andrew Ireland
Keywords
software engineering, static analysis, formal verification
Degrees
Master of Engineering in Software Engineering
Back to List