Kontaktoplysninger

Kasper Svendsen

Forskningsinstitution

Aarhus Universitet, Institut for Datalogi og University of Cambridge, Computer Laboratory, Faculty of Computer Science and Technology.

Forskningsprojekt

Programverifikation for realistiske programmeringssprog.

Forskertalent

Kasper Svendsen

Postdoc, ph.d, født 1985

Fagområde

Datalogi

Hvad handler dit projekt om?

På trods af at computere og software er designet af mennesker, og at vi i princippet ved, hvordan de fungerer, er det overraskende svært at sikre, at software fungerer korrekt. Det er især tilfældet for parallelle programmer, der består af flere beregninger, som udføres samtidigt og kommunikerer med hinanden for at løse en fælles opgave. For at kunne udføre beregninger hurtigere og med et lavere energiforbrug udfører moderne computere en række optimeringer. Disse optimeringer gør det svært selv for eksperter at sikre korrekthed af parallelle programmer. Indtil nu har de fleste metoder til at sikre korrekthed af software benyttet idealiserede hukommelsesmodeller, der ikke tager højde for disse optimeringer. De kan derfor ikke fange fejl, der skyldes de optimeringer som udføres af moderne computere. Mit projekt handler om at udvikle matematiske metoder til at sikre, at programmer fungerer korrekt for realistiske hukommelsesmodeller.

Hvordan opstod din interesse for dit forskningsfelt?

Min interesse for programverifikation opstod igennem en fascination for formel logik. Formel logik tillader, at matematiske beviser kan formuleres så præcist, at en computer kan afgøre korrektheden af et bevis uden at forstå det udsagn, der bevises. Programverifikation har givet mig rig mulighed for at udforske denne fascination, og det meste af min forskning handler om at udvikle nye og bedre logikker til at beskrive og bevise egenskaber om software. 

Hvad er de forskningsmæssige udfordringer og perspektiver ved dit projekt?

Vi er i stigende grad afhængige af den software, der blandt andet styrer de banksystemer, kommunikationssystemer, som vi alle sammen benytter i vores dagligdag. Det har længe været et mål indenfor datalogi at sikre, at sådanne systemer fungerer korrekt ved at beskrive den forventede opførsel matematisk og bevise, at den egentlige opførsel opfylder denne specifikation. Indenfor de seneste 10 år har vi gjort store fremskridt i retning af at realisere dette mål i form af nye teknikker til at beskrive og bevise egenskaber om software, der skalerer til store programmer. Men disse teknikker er stadig baseret på meget idealiserede programmeringssprog og maskinmodeller, der er meget simplere end virkelighedens programmeringssprog og computere. Mit projekt er et skridt mod mere realistiske modeller og dermed praktisk anvendelige teknikker til at bevise korrekthed for software.

Hvad vil det betyde for din forskerkarriere, at du indgår i Sapere Aude-programmet?

Sapere Aude-programmet vil give mig nye muligheder for at udvide mit internationale netværk og samarbejde med førende forskere indenfor mit felt. Min bevilling giver mig mulighed for at finansiere længere forskningsophold i udlandet til gavn for både mit projekt og fremtidige forskerkarriere.

Forskningsprojektets videnskabelige titel

Program Logics for Relaxed Memory Models.

Lidt om mennesket bag forskeren

I min fritid holder jeg af at klatre (bouldering) og eksperimentere med molekylær gastronomi i køkkenet.

Gymnasium og bopælskommune

Student fra Lyngby HTX og bopæl i Cambridge, England.