De studerende lærer at anvende centrale datalogiske modeller og formalismer, at udvikle værktøjer baseret på disse formalismer og at bruge disse værktøjer til at analysere softwarekode. En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:

• anføre forskelle i udtrykskraft af de præsenterede formelle modeller;
• tolke betydningen af en formel model (f.eks. automater, grammatiker, semantikker):
• udlede en formel model (f.eks. automater, grammatiker, semantikker) for en ønsket egenskab eller opførsel givet som en tekstuel beskrivelse;
• oversætte en model til en anden model (f.eks. regulære udtryk til NFA);
• ændre en model svarende til et givet kriterie (f.eks. fjernelse af afskedigelser, fjernelse af uklarheder grammatik);
• anvende udvalgte værktøjer og udvikle ny værktøjer relateret til de formelle modeller (f.eks. lexere, parsere, analysatorer);
• udlede egenskaber ved at anvende bevisstrategier (f.eks. matematisk induktion, strukturel induktion);
• udlede egenskaber ved at anvende bevisstrategier (f.eks. matematisk induktion, givne sætninger);
• vælge formelle modeller der kan være nødvendige eller nyttige ved løsning af et givent problem;
• opnå kursets mål som del af en gruppe, mens det individuelle ansvar opretholdes;
• kommunikere sine konstruktioner og løsninger på en klar og præcis måde; og
• demonstrere evnen til at bruge de on-line digitale lærings systemet til at forankre læringen.

Kurset omfatter to emner:

(1) Formelle sprog og deres brug til at beskrive syntaks. For regulære sprog behandles måder at beskrive dem med automata og regulære udtryk, deres sammehæng, praktiske anvendelser (fx søgning, leksikalsk analyse, formelle specifikationer). For kontekstfri sprog behandles måder at beskrive dem med pushdown automata og kontekstfri grammatik, en række anvendelser (fx til parsing af programmer, dokumenter og formateret data) sammen med en kort indføring til stakautomater og deres sammenhæng med kontekstfri sprog.

(2) Formelle metoder og deres brug til både modellering og analyse af IT systemers egenskaber, især software koe. Dette inkluderer semantik af programmeringssprog og deres brug til at bygge en compiler.

Kurset involverer praktisk brug af forskellige værktøjer, og de studerende skal løse både teoretiske og praktiske opgaver, som integrerer kursets to emner.

Mens 02141 giver en dyb behandling og praktisk erfaring med forskellige formelle metoder til at analysere programmer (programverifikation, programanalyse, informationsflowsikkerhed og modelkontrol), vil dette kursus give en kort oversigtsforelæsning om formelle metoder og deres applikationer til at bygge høje - kvalitets IT-systemer. Studerende er velkomne til at tage den fulde version (02141), som vil tælle som et 5 ETCS valgfag oven i <nyt nummer>. (1) "Introduction to Automata Theory, Languages, and Computation", af John E. Hopcroft, Rajeev Motwani, Jefrey D. Ullman, Third Edition, Addison-Wesley, 2007.
Kursusbogen "02141: Automata Theory and Languages" udvalgt af Hanne Riis Nielson indeholder de nødvendige kapitler.
(2) "Formal Methods - An Appetizer" af Flemming Nielson og Hanne Riis Nielson, Springer, 2019. Kurset gives på engelsk. 31. maj, 2023