Aarhus University Seal / Aarhus Universitets segl

Provably correct software at the push of a button

PhD defence, Wednesday 13 November 2019. Kristoffer Just Arndal Andersen.

2019.11.13 | Sunitha Satkunam

Kristoffer Just Arndal Andersen

During his studies, Kristoffer Just Arndal Andersen researched approaches to automating the use of formal methods for verification of concurrent software. Together with his colleagues in the Logic & Semantics research group, he developed tools that determine whether a concrete implementation meets an abstract specification of correct program behaviour. The last two decades of fruitful research in program logics have given us powerful, expressive methods for reasoning about concurrent and distributed programs.

The price of the added power is increased complexity -- and sheer size -- of the required mathematical arguments.

This thesis presents two different approaches to assisting the developer of software in using formal methods by way of two different tools, Caper and "Distributed Protlet Combinators" (DPC); tools that automate parts of the formal verification process for fine-grained concurrent and distributed programs, respectively. Kristoffer's research has contributed to showing the feasibility of automating reasoning in sophisticated program logics to aid the development of correct, bug-free software.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.

This résumé was prepared by the PhD student.

Time: Wednesday 13 November 2019 at 13.00
Place: Building 5335, room 295, Nygaard-295, Department of Computer Science, Aarhus University, Finlandsgade 21, 8200 Aarhus N
Title of PhD thesis: Automatic Program Verification
Contact information: Kristoffer Just Arndal Andersen, e-mail: kja@cs.au.dk, tel.: +45 23986950
Members of the assessment committee:
Professor Marieke Huisman, Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands
Associate Professor Bart Jacobs, Department of Computer Science, Katholieke Universiteit Leuven, Belgium
Professor Ira Assent, Department of Computer Science, Aarhus University (chair)
Main supervisor:
Professor Lars Birkedal, Department of Computer Science, Aarhus University
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 Science and Technology/GSST, Ny Munkegade 120, building 1521, 8000 Aarhus C.

PhD defence
12183 / i43