At give de studerende en introduktion til formelle modeller og deres anvendelser inden for konstruktion og validering af sikre og pålidelige systemer.
Kursusindhold:
Kurset spænder fra teoretiske modeller med tilhørende bevis principper til konstruktion af programmel. Kurset består af følgende dele:
Semantik: Naturlig semantik og struktural operationel semantik for et udvalg af gængse programmeringskonstruktioner. Bevis teknikker. Anvendelser i form af konstruktion af sikre og pålidelige oversættere og analyse værktøjer. Prototype implementationer af fortolkere, oversættere og analyse værktøjer.
Beregnelighed: Turingmaskiner og uafgørlige problemer. Turingmaskine modeller, non-determinisme, ækvivalensresultater, universel Turingmaskine, rekursive og rekursivt enumerable sprog. Uafgørlige problemer for Turingmaskiner og andre uafgørlige problemer, herunder reduktionsteknikker og Rices sætning.
Bemærkninger:
Forudsætninger: Beherskelse af programmering i imperative og/eller 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.
