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: gregersen@cs.au.dk, 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

Main supervisor:
Lars Birkedal, Department of Computer Science, Aarhus University, Denmark

Co-supervisor:
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.