Talk for a UQ Computing Society and MSS collaboration event, delivered on 20/05/2022.
Formal methods is a long studied (though only recently appreciated) field marrying mathematics and computer science, that concerns itself with reasoning about programs. It sees applications on topics ranging from verification of software to binary analysis and code generation.
This talk serves as an introduction to the field, with a worked example of writing an algorithm from specification alone!
- CSSE3100 - "Reasoning About Programs" (good course)
- by extension, Graeme Smith and Kirsten Winter
- "Program Proofs" by K. Rustan, M. Leino
- "Communicating Sequential Processes" by Tony Hoare