Högskola och universitet hos Göteborgs universitet, 7,5 högskolepoäng.
Formella metoder är matematiska tekniker för specifikation, design och verifiering av mjukvaru- och hårdvarusystem. I säkerhetssammanhang tillhandahåller formella metoder rigorösa verktyg för att modellera och analysera system med avseende på potentiella sårbarheter samt för att säkerställa efterlevnad av säkerhetspolicys. Dessa metoder möjliggör en exakt definition av säkerhetsegenskaper och tillåter automatiserad verifiering för att upptäcka brister som kan förbises vid traditionell testning. Genom att tillämpa formella tekniker såsom modellkontroll, satsbevisning och formella specifikationsspråk kan utvecklare bygga system med bevisbara säkerhetsgarantier. Kursen består av en serie föreläsningar om olika formalism och verifieringsmetoder som har utvecklats för att resonera kring säkerhets- och sekretessegenskaper.