View Proposal

---

Proposer

Kathrin Stark

Title

How to ensure a program has never bugs? (Program Verification)

Goal

Description

From security protocols used in online banking, over embedded control systems, to e-mail and disk encryption: every day, we use software we rely on to be safe and secure. Many things can go wrong: there might be bugs in the program itself or the compiler can produce wrong machine code. Formal verification of a program allows us to prove indisputably – using only a small set of assumptions and deduction rules – that all inputs lead to the desired behaviour. This guarantee is particularly important if faulty software would lead to a significant loss or if the software has to withstand a determined attacker. For realistic programs, verifying rich specifications beyond shallow properties such as no out-of-bound array subscripts in a fully automated way is challenging due to the immense search space. Interactive proof assistants such as Coq or Isabelle allow humans to fill in where fully automated methods fail by allowing such proofs to be developed in an interaction between humans and computers. For this reason, proof assistants have recently gained importance also in industrial applications and are used by companies like Microsoft, Amazon, Apple, and Google. I'm looking for students who are interested in learning about the verification of programs. I also have ideas of variable difficulty from current research projects. Let's talk! If you are interested in this project or would like to discuss your own project ideas, please contact me at [k.stark@hw.ac.uk](mailto:k.stark@hw.ac.uk) or make a short appointment at https://outlook.office365.com/owa/calendar/KathrinsMeetingCalendar@heriotwatt.onmicrosoft.com/bookings/.

Resources

Background

Url

Difficulty Level

Variable

Ethical Approval

None

Number Of Students

1

Supervisor

Kathrin Stark

Keywords

Degrees