FDD3461 Interaktiv teorembevisning 4,5 hp

Mjukvaru- och hårdvarusystem blir mer och mer komplexa och därmed svårare att producera med givna krav på säkerhet och tillförlitlighet. Samtidigt blir vi som individer, som organisationer och företag, och som samhälle mer och mer beroende av dem. Genom att ge stöd för modellering och verifikation ger interaktiv teorembevisning viktig stöd i framtagandet av korrekta, säkra, och tillförlitliga system. Kursen ger en översikt över olika tekniker för interaktiv teorembevisning och ger en introduktion till ett sådant verktyg i tillräckligt djup för att de studerande ska kunna genomföra en mindre modellerings- och verifikationsövning på egen hand. De studerande lär sig att formellt modellera komplexa system, att verifiera modellerna mot deras förlagor i verkligheten, samt att använda en interaktiv teorembevisare till olika former för modellanalyser.  

Vid kursens slut ska den studerande ha uppnått följande färdigheter:

 - Redogöra för olika tekniker för interaktiv teorembevisning

 - Bedöma vilka typer av problem interaktiv teorembevisning är lämpad att lösa

 - Bemästra en interaktiv teorembevisare i detalj och redogöra för dess funktion och begränsningar

 - Använda teorembevisaren korrekt på ett mindre projekt

 - Enkelt ta till sig användningen av besläktade verktyg

 - Kunna utveckla egna formella modeller och redogöra för begränsningar och tillämpbarhet, samt uttrycka och formellt bevisa viktiga modellegenskaper i teorembevisaren

 - Kunna designa och utföra grundläggande konformitetstestning

 - Funktionell programmering

 - Propositionell 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, 4,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.

Projektarbete och kursaktivitet

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.