Verification

The foremost concern in the design and implementation of any software system is correctness: does it actually do what you intend it to do? Verification addresses two problems:

• How can we formally describe the properties we want the system to have?
• How can we prove that our system has them?

And for practical use there is also a third:

• How can this be seamlessly integrated into the code development process?

Our researchers study a range of formal methods of software development and their application to real-world systems. These include:

• Session types: the specification and verification of communication protocols for concurrent and distributed computing based on type systems.
• Separation logic: this was the first logic to be used regularly on the entire code-bases of major companies to locate and eliminate memory violations.
• Game semantics: the use of game semantics as a verification framework for higher-order programming with effects.