Project Abstract

As software becomes increasingly embedded in safety-critical systems like healthcare and transportation, ensuring algorithms work correctly is more important than ever. Traditional testing often fails to catch subtle or edge-case errors, which can have serious consequences. This project explores the use of Dafny—a programming language with built-in formal verification—to address this challenge by detecting logical errors at the code level before deployment. The core aim of this research is to evaluate Dafny’s effectiveness in verifying the correctness of algorithms through real-world examples. The project uniquely positions Dafny as a middle ground between heavy manual proof systems like Coq and runtime-checking tools like Ada, investigating whether Dafny can offer a practical and scalable solution for developers new to formal methods. The approach is hands-on and iterative, beginning with the implementation of two algorithms: linear search and Dijkstra’s algorithm. Each is enhanced step-by-step with Dafny’s verification tools, including preconditions to validate inputs, postconditions to confirm outputs, and loop invariants to ensure correct behavior through iterations. Although the project is ongoing, the expected outcome is the successful formal verification of both algorithms, supported by clear specifications that prevent common coding mistakes. Key insights are anticipated in how Dafny balances automation with user control and how it compares in usability and rigor to other tools. If successful, this research will demonstrate that formal verification can be approachable and practical, not just academic. It will contribute concrete examples of verified algorithms and offer guidance on when and how Dafny is best used, helping bridge the gap between theory and industry practice.

Keywords: Formal Verification, Verified Algorithms, Dafny Programming Language

 Conference Details

Session: A

Location: Sir Stanley Clarke Auditorium at 11:00 13:00

Markers: Monika Seisenberger, Cécilia Pradic

Course: BSc Computer Science 3yr FT

Future Plans: I’m looking for an industry placement