DD3461 Interaktiv teorembevisning 4,5 hp

Interactive Theorem Proving

  • Utbildningsnivå

    Forskarnivå
  • Huvudområde

  • Betygsskala

    P, F

Det finns inget planerat kurstillfälle.

Lärandemål

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

Kursens huvudsakliga innehåll

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.  

Behörighet

 - Funktionell programmering

 - Propositionell och första ordningens logik

Litteratur

- Handbook of Practical Logic and Automated Reasoning

- Logicomix - An Epic Search for Truth (http://www.logicomix.com)

Examination

  • EXA1 - Examination, 4,5, betygsskala: P, F

Projektarbete och kursaktivitet

Ges av

EECS/Teoretisk datalogi

Examinator

Mads Dam <mfd@kth.se>

Versionsinformation

Kursplan gäller från och med VT2017.
Examinationsinformation gäller från och med VT2019.