Computing Science

Formella metoder

Enheten 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

Forskningen fokus ligger 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

Enhetens forskning är inriktad på 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 enhetens forskningsområden är typteori. Några delområden är implementering av bevisassistenter, till exempel bevisassistenten Agda, homotopi-typteori, 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.

Medarbetare