FDD3023 Interaktiv teorembevisning och programverifiering 7,5 hp

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)

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

Masterexamen i datalogi eller motsvarande.

• Funktionell programmering
• Satslogik och första ordningens logik

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

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

Slutförande av alla hemuppgifter och godkänd presentation av slutprojektet.

Mads Dam

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