Kursplan för Formella metoder i mjukvaruutveckling

• redogöra möjligheter och begränsningar hos logikbaserade verifikationstekniker föratt bedöma och förbättra mjukvarukvalitet
  
• avgöra vad som kan och inte kan uttryckas i en given formalism för specifikationeller modellering
• avgöra vad som kan och inte kan analyseras med en given logik och bevismetod
  

• formellt uttrycka säkerhetsegenskaper och liveness hos (parallella) program
• beskriva grunderna i verifikation av säkerhetsegenskaper och liveness med hjälp av modellkontroll (model checking)
• använda verktyg som automatiserar modellkontroll av säkerhetsegenskaper
• skriva formella specifikationer för klasser i objekt-orienterade program med hjälp av kontrakt och klassinvarianter
• beskriva hur förhållandet mellan program och formell specifikation kan representeras i en programlogik
• verifiera funktionella egenskaper hos enkla program med ett verifikationsverktyg
  

• bedöma och kommunicera betydelsen och vikten av korrekthet i mjukvaruutveckling
• lösa problem relaterade till utveckling av välfungerande mjukvara genom abstraktion, modellering och rigorösa resonemang

Kursen innehåller ämnen inom modellkontroll och deduktiv verifikation.

• ett specifikationsspråk för parallella processer
• verifiering av påståenden
• synkronisering
• verifikation av säkerhets- och livenessegenskaper som är skrivna i temporal logik

För deduktiv verifikation täcker kursen följande ämnen:

• programlogik, inklusive Hoare-logik och separationslogik
• resonemang om loopar med invarianter
• verifikation av små program med programverifikationsverktyg
• tekniker som används vid verifikation av större eller komplexare program