The University of Oslo is closed. The PhD defence and trial lecture will therefore be fully digital and streamed directly using Zoom. The host of the session will moderate the technicalities while the chair of the defence will moderate the disputation.
Ex auditorio questions: the chair of the defence will invite the audience to ask ex auditorio questions either written or oral. This can be requested by clicking 'Participants -> Raise hand'.
Trial lecture
Title: "Reasoning about program correctness using program logics for concurrent software."
Main research findings
- Go is an open-source programming language developed at Google that has become the underpinning of large amounts of virtual infrastructure, especially in the area of cloud computing. Inspired by Go, this thesis analyzes a programming environment where threads synchronize with each other via the exchange of messages over channels. Go specifies this interaction on a document called the memory model, written in English. We present a mathematical interpretation of the Go memory model document. Our mathematization brings benefits. For example, it allows us to more easily relate the language's design to the language's implementation. As evidence, we were able to find and fix a non-trivial bug in the Go data-race detector. Rooted in theory, our improvements to the Go data-race detector were incorporated into release 1.16 of the language. In this thesis, we share our experience applying formal methods to a large, real-world software project.
Adjudication committee:
- Professor Tarmo Uustalu, Dept. of Computer Science, Reykjavik University, Iceland
- Professor Marieke Huisman, University of Twente, The Netherlands
- Researcher Silvia Lizeth Tapia Tarifa, Department of Informatics, University of Oslo, Norway
Supervisors
- Professor Martin Steffen, Department of Informatics, University of Oslo Norway
- Professor Olaf Owe, Department of Informatics, University of Oslo Norway
Chair of defence
- Professor Ole Hanseth, Department of Informatics, UiO
Contact information to Department: Mozhdeh Sheibani Harat