Center for Basic Research in Program Verification (CPV)

Cybersecurity is one of the grand challenges of modern society and one of the
key pillars of cybersecurity is program verification. The Center for basic research in Program Verification (CPV) develops fundamental
mathematically-based models and logics that can be used for rigourous
mathematical reasoning about correctness and security of software systems. Our
work on program verification focuses on reasoning about detailed mathematical
models of program execution, so-called semantic models. This is important since
many real software errors and security breaches stem from subtle problems in
implementations of software systems. Our focus for the coming years is to
overcome fundamental obstructions to verifying vital security properties with
current techniques and improve theories and tools so that we can establish
important security properties for realistic software systems.