FDD3023 Interaktiv teorembevisning och programverifiering 7,5 hp
Allt eftersom programvarusystem blir mer komplexa så blir det också svårare att garantera att de uppfyller givna krav på säkerhet och tillförlitlighet. Samtidigt ökar beroendet av sådana system bland individer, organisationer och hela samhällen. Interaktiva teorembevisare (ITP:er) är kraftfulla, flexibla och tillförlitliga verktyg för systemmodellering och formell verifiering. En växande användning av ITP:er är för specifikation och konstruktion av praktiska, pålitliga och storskaliga programvarusystem. Den här kursen ger en översikt av grundvalar och tekniker för ITP:er och hur de kan användas för att modellera, specificera och formellt verifiera programvarusystem, inklusive både abstrakta systemmodeller och exekverbara program.
Information för forskarstuderande om när kursen ges
Kursen kommer att ges i period 3.
Innehåll och lärandemål
Kursinnehåll
De studerande kommer att lära sig att modellera komplexa system, uttrycka sina modeller och specifikationer i ITP:ers formella språk, och använda ITP:er för att producera formella bevis för att modellerna uppfyller sina specifikationer.
Efter att ha läst kursen kommer de studerande kunna utföra sina egna modellerings- och verifieringsprojekt i en ITP, och förstå möjligheterna och begränsningarna med att använda ITP:er för programverifiering.
Kursupplägg
Kursen består av en föreläsning per vecka och veckovisa hemuppgifter som studenterna ska lösa individuellt. För att slutföra kursen måste studenterna lösa alla hemuppgifter och välja och utföra ett slutprojekt. Föreläsarna kommer att vara tillgängliga för svara på frågor om hemuppgifterna och slutprojektet under speciella tider varje vecka och i förbokade möten med individuella studenter.
Kurslitteratur
- HOL4 guidebok (https://hol-theorem-prover.org/guidebook)
- HOL4 logik (http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-logic.pdf/download)
Lärandemål
Vid kursens slut ska den studerande kunna
- Redogöra för olika grundvalar och tekniker för interaktiv teorembevisning
- Bedöma vilka typer av programverifieringsproblem en interaktiv teorembevisare är lämpad att lösa
- Redogöra för funktionalitet och begränsningar i moderna interaktiva teorembevisare
- Använda en interaktiv teorembevisare på ett korrekt sätt i ett mindre programverifieringsprojekt
- Utveckla egna formella modeller av programvarusystem i en interaktiv teorembevisare och redogöra för deras begränsningar och tillämplighet samt uttrycka och formellt bevisa viktiga modellegenskaper i verktyget
- Planera och genomföra grundläggande validering av egna formella modeller
- Genomföra grundläggande bedömning av potentiella vinster och kostnader vid tillämpning av interaktiva teorembevisare för verifiering av specifika programvarusystem
Kurslitteratur och förberedelser
Särskild behörighet
Masterexamen i datalogi eller motsvarande.
Rekommenderade förkunskaper
- Funktionell programmering
- Satslogik och första ordningens logik
Utrustning
Kurslitteratur
Examination och slutförande
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Betygsskala
Examination
- EXA1 - Examination, 7,5 hp, betygsskala: P, F
Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.
Examinator får medge annan examinationsform vid omexamination av enstaka studenter.
Examinationen består av hemuppgifter och ett slutprojekt.
Övriga krav för slutbetyg
Slutförande av alla hemuppgifter och godkänd presentation av slutprojektet.
Möjlighet till komplettering
Möjlighet till plussning
Examinator
Etiskt förhållningssätt
- Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
- Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
- Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.