Faglige nøgleord: Programmering, programmeringssprog, safety-critical systems, programverifikation, computernetværk, digital kommunikation
Oplæg tilgængeligt på: Dansk og engelsk
I denne moderne, højteknologiske verden vil man gerne sikre, at programmer virker, som de skal – inden de køres. Der er flere motiverende eksempler: flycomputere, atomreaktorer, og andre såkaldte "safety-critical systems", der skal virke korrekt i første omgang. Selv i mindre "alvorlige" systemer som f.eks. banksystemer og shoppingsider kan fejl føre til nedbrud, som igen kan medføre høje omkostninger og besvær for både brugerne og ejerne af systemet.
Men hvordan sikrer man denne korrekthed? Man kan selvfølgelig gå empirisk til værks, med uddybende tests, møjsommelig gennemlæsning af programmet, og så videre. For nogle systemer er dette overbevisende nok, men selv grundige efterprøvninger kan have blinde vinkler, og giver derfor ikke 100% garanti for korrekthed. I denne præsentation vil jeg vise, hvordan man med en anden tilgang kan opnå denne garanti. Helt specifikt drejer det sig om at bevise (altså i en matematisk forstand), at et program virker. Dette er, hvad min forskning i grove træk går ud på. Min forskning omhandler mere specifikt, hvordan man kan designe et programmeringssprog således, at et program kodet i det altid vil opføre sig på en bestemt måde.
Min præsentation kommer, ud over mit forskningsområde, også til at omhandle faget datalogi helt generelt, men set fra en matematisk/teoretisk vinkel fremfor en mere ingeniørfaglig/praktisk vinkel; dog selvfølgelig holdt på gymnasieniveau. Derudover kommer jeg også til at supplere med praktiske eksempler, øvelser, og min egen fortælling om, hvordan jeg gik fra gymnasiet til en ph.d.
Jeg startede selv på H.C. Ørsted Gymnasiet i Kgs. Lyngby (HTX), hvor jeg blev student i 2016. Jeg fortsatte derefter med at tage min bachelor og kandidat indenfor datalogi på Københavns Universitet, som jeg afsluttede i 2021. Efter et års arbejde som forskningsassistent begyndte jeg så på min ph.d. på DTU.