Computing Science

Avdelningen för Computing Science bedriver forskning och utbildning som främjar utformningen av säkra och tillförlitliga program och system, från teoretiska grunder och uppåt genom design och implementering av programmeringsspråk och verktyg. 

Enheter

Formella metoder

Gruppen bedriver forskning kring användningen av matematiska och logikbaserade tekniker för specifikation och verifiering av system. Gruppen ä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

Gruppen fokuserar på tillämpningen av programmeringstekniker, och i synnerhet funktionella tekniker, för att lösa praktiska problem. Gruppen är mest känd för sitt arbete med domänspecifika språk, hårdvaruverifikation, mjukvarutestning och (formella och naturliga) språkteknologier. Deras forskning har utöver forskningspublikationer resulterat i två spinoff-företag.

Informationssäkerhet

Gruppen 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. Gruppen ä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
Gruppen arbetar med typteori: å ena sidan teoretiska undersökningar av syntax och semantik, å andra sidan implementering och tillämpningar av bevisassistenter. Gruppen har utvecklat flera kända bevisassistenter, till exempel Agda-systemet. Den har också på ett avgörande sätt bidragit till att formulera logiska system för beroendetyper och att undersöka dem meta-teoretiskt.

Medarbetare

Avdelningschef: David Sands​

Sidansvarig Publicerad: to 30 dec 2021.