Center for Grundforskning i Programverificering (CPV)

Cybersecurity er en af de største udfordringer for vores moderne samfund og en af hjørnestenene for cybersecurity er programverifikation. Center for grundforskning i programverificering (CPV) vil udvikle fundamentale matematiskbaserede modeller og logikker som kan bruges til formel matematisk ræsonnering om korrekthed og sikkerhed for softwaresystemer. Vores arbejde fokuserer på detaljerede, såkaldte semantiske, modeller for programudførelse. Det er vigtigt eftersom en stor del af softwarefejl og sikkerhedsbrister skyldes subtile problemer i implementationen af softwaresystemer. Vores fokus i de kommende år er at finde løsninger på en række fundamentale begrænsninger for nuværende state-of-the-art og dermed forbedre teorier og værktøjer så vi kan bevise vigtige sikkerhedsegenskaber for realistiske softwaresystemer.