Aarhus University Seal / Aarhus Universitets segl

Med et tryk på en knap: beviseligt korrekt software

Ph.d.-forsvar, onsdag den 13. november 2019. Kristoffer Just Arndal Andersen.

13.11.2019 | Sunitha Satkunam

Kristoffer Just Arndal Andersen

I løbet af sit ph.d. Studium har cand.scient. Kristoffer Just Arndal Andersen forsket i automatisering af matematiske metoder til at påvise korrektheden af samtidige programmer – programmer der kører flere beregninger på samme tid. Med sine kollegaer i forskningsgruppen Logik & Semantik har Kristoffer udviklet værktøjer, der med en beskrivelse af et programs ønskede opførsel forsøger at afgøre om en konkret implementation lever op til forventningerne. De seneste 20 års succesfuld forskning i matematikken bag flertrådet og distribuerede programmer har givet os kraftfulde matematiske systemer til at udtrykke og ræsonnere omkring sådanne programmer - såkaldte “programlogikker”.

Prisen for denne udtrykskraft er øget kompleksitet af de involverede matematiske argumenter.

Ph.d.-afhandlingen demonstrerer to tilgange til at håndtere sådanne beviser ved hjælp af automatiske værktøjer, “Caper” og “Distributed Protlet Combinators” (DPC), der hjælper softwareudviklere med bevisførelsen for korrektheden af hhv. Flertrådet og distribuerede programmer. Kristoffer har med de opnåede resultater demonstreret anvendeligheden af matematisk velfunderet teknikker i skabelsen af effektive værktøjer til udvikling af korrekt, fejlfri software.

Ph.d.-studiet er gennemført ved Institut for Datalogi, Science and Technology, Aarhus Universitet.

Dette resumé er udarbejdet af den ph.d.-studerende.

Tid: Onsdag den 13. november 2019, kl 13.00
Sted: Bygning 5335, lokale 295, Nygaard-295, Institut for Datalogi, Aarhus Universitet, Finlandsgade 21, 8200 Aarhus N
Afhandlingens titel: Automatic Program Verification
Kontaktinfo: Kristoffer Just Arndal Andersen, e-mail: kja@cs.au.dk, tlf.: 23986950
Bedømmelsesudvalg:
Professor Marieke Huisman, Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, Holland
Associate Professor Bart Jacobs, Department of Computer Science, Katholieke Universiteit Leuven, Belgien
Professor Ira Assent, Department of Computer Science, Aarhus Universitet (formand)
Hovedvejleder:
Professor Lars Birkedal, Institut for Datalogi, Aarhus Universitet
Sprog: Ph.d.-afhandlingen forsvares på engelsk

Forsvaret er offentligt.
Afhandlingen ligger til gennemsyn hos Graduate School of Science and Technology/GSST, Ny Munkegade 120, bygning 1521, 8000 Aarhus C.

PhD defence