Enkeltfag Engelsk 7.5 ECTS

Programverifikation

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.

See course description in English

Læringsmål

  • 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.

Anbefalede forudsætninger

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.

Undervisningsform

Forelæsninger, øvelser og projektarbejde.

Fakultet

Se kurset i kursusbasen

Tilmelding

Sprog

Engelsk

Varighed

13 uger

Institut

Compute

Sted

DTU Lyngby Campus

Kursus ID 02245
Kursustype Kandidat
Semesterstart Uge 35
Semester slut Uge 48
Dage tors 13-17
Pris

11.250,00 kr.

Tilmelding