Avdelningen är uppdelad i fyra enheter som bedriver forskning och utbildning som främjar utformningen av säkra och tillförlitliga program och system, från teoretiska grunder till design och implementering av programmeringsspråk och verktyg.
Formella metoder
Bedriver forskning kring användningen av matematiska och logikbaserade tekniker för specifikation och verifiering av system. Enheten är mest känd för sitt arbete med (automatisk och interaktiv) teorembevisning, deduktiv verifiering, verifierad kompilering, reaktiv syntes från temporal logik, runtime-verifiering och formell analys av normativa system.
Funktionell programmering
Fokuserar på tillämpningen av programmeringstekniker, och i synnerhet funktionella tekniker, för att lösa praktiska problem. Enheten är mest känd för sitt arbete med domänspecifika språk, hårdvaruverifikation, mjukvarutestning och (formella och naturliga) språkteknologier. Forskningen har utöver forskningspublikationer resulterat i två spinoff-företag.
Informationssäkerhet
Bedriver forskning inom säkerhet och integritet, språkbaserad säkerhet, datasekretess med hjälp av en rad tekniker, såsom differentiell integritet och integritetsbevarande platstjänster. Enheten är känd för sitt arbete med informationsflödessäkerhet, webbsäkerhet och säkerhetsstiftelser. Gruppen är en del av Chalmers Security Lab.
Logik och typer
Arbetar med typteori: å ena sidan teoretiska undersökningar av syntax och semantik, å andra sidan implementering och tillämpningar av bevisassistenter. Enheten har utvecklat flera kända bevisassistenter, till exempel Agda-systemet, och har på ett avgörande sätt bidragit till att formulera logiska system för beroendetyper och att undersöka dem meta-teoretiskt.
