Scalable Mathematics for Computer Programs to Prove Computer Programs Correct
PhD defence, Friday 17 March 2023. Simon Oddershede Gregersen
It is a complicated matter to establish with certainty that software always does what it ought to do, and more so if we want to prove with mathematical rigor that the actual program code---and not only the algorithm---is correct. To do so, we need to use elaborate models of program execution. Still, as software systems grow larger and larger, these models become unfeasible to reason about by hand due to their sheer size and complexity. Therefore, we need powerful mathematical machinery to alleviate this complexity and to make the computers themselves help us prove our programs correct!
During his Ph.D. studies, Simon Oddershede Gregersen has been developing new theories and mathematical tools, so-called program logics, for computer-assisted reasoning about computer programs. In particular, his research has made significant progress on expressive and scalable methods in the context of network-connected distributed applications, randomization, and information-flow security.
The PhD study was completed at Department of Computer Science, Faculty of Natural Sciences, Aarhus University.
This summary was prepared by the PhD student.
Time: Friday 17 March 2023 at 13.00
Place: Building 5510, room 104, small auditorium, InCuba, Aarhus University, Åbogade 15, 8200 Aarhus N
Title of PhD thesis: Higher-Order Separation Logic for Distributed Systems and Security
Contact information: Simon Oddershede Gregersen, e-mail: firstname.lastname@example.org, tel.: +45 2140 5661
Members of the assessment committee:
Professor Deepak Garg, Max Planck Institute for Software Systems, Germany
Professor François Pottier, Inria, National Institute for Research in Digital Science and Technology, France
Associate Professor Peyman Afshani (Chair), Department of Computer Science, Aarhus University
Lars Birkedal, Department of Computer Science, Aarhus University, Denmark
Amin Timany, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in English
The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS,
Jens Baggesens Vej 53, building 5221, 8200 Aarhus N.