De studerende lærer at anvende de centrale modeller der bliver introduceret i løbet af kurset og at bruge software værktøjer relateret til disse formalismer. 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 given beskrivelse i en formel model (f.eks. automater, grammatiker, semantikker):
• udlede en beskrivelse i en formel model (f.eks. automater, grammatiker, semantikker) for en ønsket egenskab eller opførsel givet som en tekstuel beskrivelse;
• oversætte til en anden model (f.eks. regulære udtryk til NFA);
• ændre en given beskrivelse svarende til et givet kriterie (f.eks. fjernelse af ubrugelige produktioner, tilføjelse af sprogkonstruktioner);
• anvende udvalgte værktøjer relateret til de formelle modeller (f.eks. lexere, parsere);
• afgøre om en beskrivelse i en formel model opfylder en givet egenskab;
• 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 systemer på FormalMethods.dk til at forankre læringen.

Kurset omfatter to emner:

(1) Formelle sprog og deres brug til at beskrive syntaks. For regulære sprog behandles deres sammehæng med endelige automater, praktiske anvendelser (fx søgning, leksikalsk analyse) og nogle væsentlige teoretiske resultater (herunder lukketheds- og afgørlighedsegenskaber). For kontekstfri sprog behandles en række anvendelser (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. Herunder semantik og fortolkning, programanalyse, sikkerhedsanalyser, og modeltjek. Systemerne på FormalMethods.dk bruges til at understøtte indlæringen.

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. (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. Videoer på YouTube kanalen FormalMethodsDK. Slides og on-line systemer på FormalMethods.dk Kurset gives på engelsk. 15. marts, 2021