At give de studerende en introduktion til formelle teknikker og deres anvendelser inden for semantik og beregnelighed.
Kursusindhold:
Semantik: Transitions systemer, naturlig semantik og struktural operationel semantik. Type systemer, herunder polymorfi. Semantik for imperative, procedurale og funktionssprog. Prototype implementationer. Programanalyse: Monotone og distributive rammer. Gitterteori og Tarskis fixpunkt teorem. Semantisk korrekthed. Fremad, baglæns, første ordens og anden ordens programanalyser. Algoritmer for constraint solving. Optimerende oversættere og validering af sikkerhedsegenskaber. Beregenlighed: Turingmaskiner og uafgørlige problemer. Turingmaskine modeller, non-determinisme, ækvivalensresultater, universel Turingmaskine, rekursive and rekursivt enumerable sprog. Uafgørlige problemer for Turingmaskiner og andre uafgørlige problemer, herunde reduktionsteknikker og Rices teorem.
Bemærkninger:
Forudsætninger: Beherskelse af programmering i imperative og funktionelle sprog; herunder algoritmer og datastrukturer. Forståelse af teori og anvendelser af regulære og kontekstfrie sprog; herunder diskret matematik med færdigheder i simple bevisteknikker. Kan opnås i Informatik fagpakken med tilhørende startpakken.
