Aarhus University Seal / Aarhus Universitets segl



  • Center for Basic Research in Program Verification

Software systems are an integral part of modern society, and software errors and security breaches pose enormous costs and risks. Center for basic research in Program Verification (CPV) develops fundamental mathematically based models and logics for rigorous mathematical reasoning about correctness and security of software systems.

To analyze and reason about software systems it is important to consider models at many different levels of abstraction. Since many real software errors and security breaches stem from subtle problems in implementations of software systems, CPV focus on detailed, so-called semantic, models of program execution.

CPV builds on several recent breakthrough results, by researchers from Department of Computer Science at Aarhus University, in program verification for modern software systems.


Welcome to new Postdoc Alejandro Aguirre

2021.04.01Welcome to Alejandro Aguirre, who joins CPV as a Postdoc from April 1, 2021. Alejandro obtained his PhD from the Technical University of Madrid in February 2021. During his studies, he worked as a predoctoral researcher at the IMDEA Software Institute, under the supervision of Professor Gilles…

Inaugural lecture by Amin Timany

2021.03.26On April 9, Assistant professor Amin Timany will give his inaugural lecture on Zoom. Title: Formal reasoning about programs and programming languages. Abstract: It is well known that it is important to ensure that programs, especially in critical applications, e.g., online banking, are correct.…

Lars Birkedal. Photo: VillumFonden

Amazon Research Award to Lars Birkedal

2021.03.15Congratulations to Lars Birkedal who has received an $80,000 Amazon Research Award (ARA). The grant will support the research already being done at Centre for Center for basic research in Program Verification (CPV), in which Lars and his team develop fundamental mathematically based models and…

Great success for LogSem and PL at two top conferences

2020.11.16Researchers from Logic & Semantics and Programming Languages have had a remarkably high number of papers accepted at the top conferences OOPSLA’20 and POPL’21. At OOPSLA, which takes place this week, five papers have been accepted for publication. At POPL, they got six papers got accepted, which is…


    CPV  is currently looking for both PhD students and Postdocs

    If you are interested, please send an email to Lars Birkedal or Sofia Rasmussen.

Head of research


Center for Basic Research in Program Verification (CPV) is funded by a Villum Investigator grant (no. 25804) from The Villum Foundation from 2019-2025.

Affiliated researchers

Aslan AskarovAssociate ProfessorAarhus University
Amin TimanyAssistant Professor Aarhus University
Bas SpittersAssociate ProfessorAarhus University
Jaco van de PolProfessorAarhus University
Jon Michael Aanes Student Programmer Aarhus University