Lars Birkedal

Professor, institutleder

Lars Birkedal
Lars Birkedal
Alder

1970

Fødested, gymnasium og nuværende bopælskommune

Født på Frederiksberg, student fra Marie Kruses Skole, bopæl i Aarhus kommune. 

Fagområde

Datalogi

Institution

Institut for Datalogi, Aabogade 34, 8200 Aarhus N.

Kontaktoplysninger

Mobil: 2383 846, e-mail: birkedal@cs.au.dk

Kort beskrivelse af dit forskningsområde

Mit forskningsområde er teoretisk datalogi, nærmere bestemt logik og semantik. Dette forskningsområde omhandler udviklingen af nye matematiske modeller og teknikker til at beskrive og analysere programmer samt til at udvikle bedre programmeringssprog. Sådanne modeller og teknikker udgør fundamentet for udviklingen af software-værktøjer, som kan assistere programmører med at lave korrekt software. Dette er af stor betydning, idet det er kritisk for det moderne samfunds infrastruktur, at softwaresystemer fungerer korrekt. I dag er den mest udbredte teknik til at sikre, at programmer fungerer afprøvning, også kaldet test – programmørerne tester deres programmer på forskellige former for input data og ser, om programmerne gør som forventet. Men med test kan man ikke sikre sig, at alle fejl i programmer findes. Der er derfor behov for bedre teknikker til at sikre mod fejl i programmer, og igennem de seneste 10-15 år er der sket store forskningsfremskridt inden for udviklingen af matematisk-baserede teknikker hertil. Der er sket fremskridt inden for en række relaterede områder: Der er blevet udviklet nye grundlæggende matematiske modeller, der kan bruges til at analysere og beskrive større klasser af programmer (på samme vis som der skal bruges speciel matematik til at lave ingeniørberegninger på broer, skal der bruges speciel matematik til at analysere programmer); der er blevet udviklet bedre algoritmer til automatiske software-værktøjer baseret på matematisk logik; og der er sket store fremskridt inden for udviklingen af såkaldte bevisassistenter, som er specialiserede programmeringssprog, der kan bruges til implementering af matematiske modeller og beviser. I min forskningsgruppe har vi bl.a. udviklet nye matematiske modeller for moderne programmeringssprog og brugt nogle af disse til at lave prototype-værktøjer til programverifikation ved hjælp af bevisassistenter. 

De forskningsmæssige udfordringer og perspektiver

At udvikle korrekt og pålidelig software er særdeles vanskeligt, og det anses for at være en af de største udfordringer i datalogien. Moderne softwaresystemer er ekstremt komplekse. Programmører forsøger at håndtere kompleksiteten ved at dele store softwaresystemer op i en række programmoduler, som kan forstås hver for sig, og som kan udvikles af forskellige programmører. For logik og semantik forskning er det vigtigt, at de matematiske modeller og teknikker er tilsvarende modulære, således at teknikkerne kan skalere til store softwaresystemer. Det forskes der intensivt i over hele verden, på universiteter, i store softwarevirksomheder samt i mindre specialiserede start-up virksomheder, og nogle af teknikkerne bliver nu anvendt i industrien, for eksempel til at forbedre software til flyvemaskiner.

Der er mange forskellige forskningsudfordringer. I min forskningsgruppe har vi fokuseret på udviklingen af modulære matematiske modeller til at analysere og beskrive programmer skrevet i moderne programmeringssprog, såsom Java, C# og ML. Moderne programmeringssprog indeholder en række centrale programmeringssprogselementer, som gør det vanskeligt at lave modulære modeller, specielt delte opdaterbare datastrukturer og parallelitet. Delte opdaterbare datastrukturer er vigtige i programmering for at implementere algoritmer effektivt. Intuitivt er det vanskeligt at beskrive og analysere programmer med delte opdaterbare datastrukturer modulært, fordi man skal passe på, at et modul ikke ændrer i en datastruktur, uden at et andet modul ved det. 

Moderne computere udfører beregninger i parallel, på flere processorer på samme tid. Intuitivt er det vanskeligt at beskrive og analysere programmer med parallelitet, fordi flere processorer kan opdatere datastrukturer på samme tid, med uforudsete resultater til følge. Det problem kan man løse ved at begrænse paralleliteten ved brug af såkaldte låse, men så udnytter man ikke paralleliteten optimalt og får dermed ikke den ønskede effektivitet.

I min forskningsgruppe har vi bl.a. udviklet nye modulære matematiske modeller og teknikker, der kan bruges til at beskrive og analysere avancerede parallelle programmer, der ikke bruger låse, og som bruges som centrale komponenter i moderne softwaresystemer. På baggrund af vore modeller har vi endvidere udviklet prototype-værktøjer til delvis automatisk programverifikation, i første omgang for programmer uden parallelitet; for tiden arbejder vi på at videreudvikle disse til også at omfatte parallelle programmer.

Hvordan opstod interessen for netop dette forskningsfelt? 

Min interesse for logik og semantik startede på mit kandidatstudium på Københavns Universitet, hvor jeg studerede programmeringssprog og automatiske programanalyser. Min interesse blev styrket gennem mit ph.d.-studium på Carnegie Mellon University (USA), hvor jeg blev vejledt af Dana Scott, hovedgrundlægger af feltet logik og semantik i datalogi. Jeg blev fascineret af, hvorledes matematiske modeller for beregnelighed kan bruges til at imødekomme udfordringer i datalogien. I mit ph.d.-arbejde udviklede jeg modeller for bevisassistenter. Jeg har siden arbejdet på at udvikle nye matematiske modeller, der kan bruges til at beskrive og analysere programmer skrevet i mere udbredte moderne programmeringssprog. 

Hvordan vil du anvende EliteForsk-prisen?

Rådighedsbeløbet vil jeg bruge til at styrke vores forskning inden for udviklingen af prototype-værktøjer til programverifikation for parallelle programmer. Der er brug for at udforske forskellige former for værktøjer, spændende fra automatiserede værktøjer, som kan afhjælpe simplere klasser af fejl i programmer, til mere avancerede værktøjer, som kan bruges til at bevise fuld korrekthed af kritiske software moduler. Konkret regner jeg med at bruge størstedelen af rådighedsbeløbet til at ansætte en ung forsker, der kan samarbejde med mig og mine internationale samarbejdspartnere omkring disse udfordringer. Hædersgaven vil jeg formentlig bruge til en spændende rejse sammen med min familie, og måske også til en ny cykel.

Hvad er din reaktion på at have vundet en af de største forskningspriser i Danmark?

Jeg er meget stolt og glad for den anerkendelse EliteForsk-prisen er udtryk for. Det er naturligvis rart at mærke på en sådan konkret vis, at den forskningsindsats, min forskningsgruppe og jeg yder, bliver påskønnet. Min forskning foregår i samarbejde med mine ph.d.- studerende og postdocs samt et stort netværk af internationale forskere. Jeg er meget taknemmelig for det samarbejde, som er helt centralt for forskningen, og som gør det daglige arbejde til en fornøjelse.

Lidt om mennesket bag forskeren

Jeg er født og opvokset i Københavnsområdet, og efter mit datalogistudie i København flyttede jeg til USA, hvor jeg læste til ph.d. og boede i 5 1/2 år. I år 2000 flyttede min hustru, Merete, og jeg tilbage til Danmark. Merete er også forsker, og hun fik arbejde på Københavns Universitet, og jeg fik arbejde på IT-Universitetet. Merete og jeg har to fantastiske børn, Mathias (14 år) og Sofia (11 år), som er meget glade for sport og musik. I januar 2013 flyttede hele familien til Aarhus, hvor vi nu bor i Risskov, i kort afstand til Aarhus Universitet, hvor både Merete og jeg arbejder. Jeg holder meget af at cykle, løbe og lave mad. Jeg nyder også at rejse med familien, gerne på varieret vis (ski, vandre, nationalparker etc.).

Argument for tildeling af pris

Lars Birkedal forsker indenfor teoretisk datalogi og er international førende indenfor logik og semantik af programmeringssprog. Han har udviklet matematiske modeller til verifikation og analyse af programmeringssprog og har været en pioner i udviklingen af prototype værktøjer til programverifikation. Hans arbejde er banebrydende og af uvurderlig betydning for forståelsen af moderne komplekse programmeringssprog.

Lars Birkedal har et meget stort international samarbejdsnetværk og adskillige både nationale og internationale tillidshverv. Lars Birkedals imponerende produktion omfatter næsten 100 publikationer, som er citeret næsten 2800 gange. Et imponerende stort antal af hans publikationer er blevet valgt som ”best paper” ved de internationalt førende datalogikonferencer.

Lars Birkedal blev kandidat fra Københavns Universitet i 1994 og ph.d. fra Carnegie Melon Universitet i 1999. Han blev derefter adjunkt ved IT-Universitetet og siden lektor og professor samme sted i 2008. Siden 2013 har han været professor ved Aarhus Universitet, hvor han leder forskningsgruppen i logik og semantik. Han modtog i 2013 en af Det Frie Forskningsråds Sapere Aude topforsker bevillinger.

Senest opdateret 27. januar 2016