02245 Programverifikation

2024/2025

Kursusinformation
Program Verification
Engelsk
7,5
Kandidat
Retningsspecifikt kursus (MSc), Computer Science and Engineering
Teknologisk specialisering (MSc), Computer Science and Engineering
E1B (tors 13-17)
Online
Forelæsninger, øvelser og projektarbejde.
13-uger
E1B, Afhængigt af antallet af studerende kan der være behov for også at aftale andre dage.
Mundtlig eksamen og bedømmelse af rapport(er)
En eller to rapporter danner grundlag for den mundtlige eksamen.
Alle hjælpemidler - med adgang til internettet
7-trins skala , ekstern censur
02141 , Grundlæggende kendskab til programsemantik og prædikatlogik er forventet. Den nødvendige viden kan opnås i 02141. Den studerende skal beherske mindst ét objekt-orienteret eller funktionelt programmeringssprog. Kurser i matematisk logik, f.eks. 02156, er en fordel.
Christoph Matheja , chmat@dtu.dk
Alberto Lluch Lafuente , Lyngby Campus, Bygning 321, Tlf. (+45) 4525 3736 , albl@dtu.dk
01 Institut for Matematik og Computer Science
http://courses.compute.dtu.dk/02245/
I studieplanlæggeren
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
02. maj, 2024