Overordnede kursusmål
Dette kursus tilbyder en praktisk introduktion til brug og
konstruktion af automatiske og deduktive
programverifikationsværktøjer samt til teorien bag disse. Den
studerende skal erhverve de nødvendige færdigheder for at kunne
anvende og udvide værktøjssupporterede metodologier til udvikling
af beviseligt korrekt software.
Læringsmål
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
- specificere de funktionelle korrekthedsegenskaber af et
funktionsrigt imperativt program;
- bruge automatiserede verifikationsværktøjer til at udvikle
formelt verificeret software;
- begrunde om et program følger sin specifikation, baseret på
sunde udledningsprincipper;
- forklare hvert lag i den teknologistak, som er involveret i
opbygningen af automatiske verifikationsværktøjer;
- sammenligne deduktiv programverifikation med andre metoder der
forsøger at øge tilliden til softwares korrekthed;
- indkode verifikationsrelaterede beslutningsproblemer i SMT
(satisfiability modulo theories);
- identificere potentielle flaskehalse i en eksisterende
SMT-indkodning;
- konstruere sunde metodologier til løsning af
programverifikationsproblemer, og automatisere disse ved hjælp af
SMT-indkodninger, samt kunne argumentere for de trufne
designvalg;
- opnå ovenstående i grupper, mens man også er individuelt
ansvarlig; og
- kommunikere løsninger til programverifikationsproblemer på en
klar og præcis måde.
Kursusindhold
Kurset dækker over de udledningsprincipper, teknologier og
designvalg, der underbygger automatiske deduktive
verifikationsværktøjer.
(1) Programlogikker til at skrive formelle korrekthedsbeviser (for
eksempel svageste forudsætning og separationslogik)
(2) SMT solvers (for eksempel Z3) til at automatisere udledningen
af logiske formler,
(3) Mellemliggende verifikationssprog (for eksempel Viper) til
indkodning af
verifikationsmetodologier, og
(4) Kildekodeverifikationsværktøjer til håndtering af funktionsrige
programmeringssprog.
Kurset vil blande teknisk og praktisk indhold.
Litteraturhenvisninger
Udvalgte bogkapitler og forskningsartikler ud over slides og
forelæsningsnoter. Det relevante materiale vil blive gjort
tilgængeligt online.
Sidst opdateret
15. september, 2023
