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 Patricia Johann & Pierre Cagne

2021.07.05We are happy to welcome visiting professor Patricia Johann from Appalachian State University. Patricia will be part of Center for Basic Research in Program Verification (CPV) from August 2021 to January 2022. Along with Patricia is her postdoc Pierre Cagne. We look forward to working with you!

Four papers accepted at CSF

2021.06.07Four papers from Logic and Semantics and CoBRA were accepted at the Computer Security Foundations Symposium (CSF). CSF is an annual conference for researchers within computer security, and will take place online from June 21-24. See the full list of accepted papers and the conference program at:…

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.…


    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