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
Det gemensamma temat för forskningen vid enheten är tillämpning av matematiska och logiska metoder på olika problem inom teoretisk datavetenskap.
Ett av forskningsområden är typteori. Några delområden är implementering av bevisassistenter, t.ex. Agda, homotopitypteori, syntetisk algebraisk geometri och tillämpningar av typteori för kvantberäkningar.
Ett annat forskningsområde är algoritmisk grafteori - i synnerhet NP-svåra grafteoretiska problem.
För mer information om enhetens forskning hänvisar vi till Logik och typers engelska webbsida.
