Under sine ph.d.-studier undersøgte Zongyuan anvendelsen af separationslogik til verifikation af lavniveau-systemer. Separationslogik er en verifikationsteknik, der sikrer softwarekorrekthed og -sikkerhed ved at tilbyde en formel ramme for modulær ræsonnering om komplekse programadfærdsmønstre. Anvendelsen af separationslogik på lavniveau-systemer er dog udfordrende, da det kræver ræsonnering om indviklede lavniveau-adfærdsmønstre, samtidig med at den overordnede modularitet bevares.

Zongyuan undersøgte separationslogik i forhold til to centrale aspekter af lavniveau-systemer: (1) virtuel hukommelse og hukommelsesdeling i systemsoftware samt (2) samtidighed i hardwarearkitekturer med "relaxed memory". Hans forskning bidrager til en dybere forståelse af separationslogik som en modulær tilgang til ræsonnering om disse komplekse problemstillinger og danner grundlaget for stringent verifikation af software i den virkelige verden.

Ph.d.-studiet er gennemført ved Institut for Datalogi, Faculty of Natural Sciences, Aarhus Universitet.

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

Tid: onsdag den 30. april 2025 kl. 13:00
Sted: Bygning 5342, lokale 333, Institut for Datalogi, Aarhus Universitet, Åbogade 34, 8200 Aarhus N.
Afhandlingens titel: Separationslogik for lavniveau- og realistiske programmer
Kontaktinfo: Zongyuan Liu, e-mail: zy.liu@cs.au.dk, tlf.: +45 50145213
Bedømmelsesudvalg:
Fastansat forsker Viktor Vafeiadis, Max Planck Institute for Software systems, Tyskland
Forskningsprofessor Aleks Nanevski, IMDEA Software Institute, Spanien
Professor Anders Møller (forperson), Institut for Datalogi, Aarhus Universitet, Danmark
Hovedvejleder: Professor Lars Birkedal, Institut for Datalogi, Aarhus Universitet, Danmark
Medvejleder: Tenure Track adjunkt Jean Pichon-Pharabod, Institut for Datalogi, Aarhus Universitet, Danmark
Sprog: Ph.d.-afhandlingen forsvares på engelsk

Forsvaret er offentligt.
Afhandlingen ligger til gennemsyn hos Graduate School of Natural Sciences (GSNS), Ny Munkegade 120, bygning 1521, 8000 Aarhus C