Our research connects the mathematical foundations of programs, programming languages, and computational systems with automated analysis and verification. As AI systems generate an increasing amount of code, independent methods for checking correctness, safety, and resource consumption are becoming ever more important. We develop models, logics, algorithms, and tools for this purpose, use machine learning to support automated reasoning, and apply logical methods to characterise the capabilities and limitations of AI models.
What does a program mean?
Formal semantics and type systems precisely describe what programs mean and which programs are admissible. We are particularly interested in how modern programming languages provide safety guarantees.
Selected topics:
- Formal semantics and type systems
- Formal models of ownership and borrowing
- Formal methods for the Rust programming language
How can programs be analysed automatically?
We develop methods that automatically infer properties of programs and make them available for verification.
Selected topics:
- Compositional shape analysis for memory-safety verification
- Separation-logic-based program analysis and biabduction
- Automated inference of resource and complexity bounds
What can be decided automatically?
We study the expressiveness, decidability, and complexity of logics, automata, and other mathematical models.
Selected topics:
- Expressiveness and decidability of fragments of separation logic
- Petri nets, or equivalently vector addition systems with states (VASS), and related infinite-state systems
- Automata and logical formalisms for graphs and computational systems
How can formal methods and AI benefit each other?
Machine learning can support formal reasoning; conversely, logical methods can help us understand AI models.
Selected topics:
- Machine-learned guidance for first-order proof search
- Logical characterisations of the expressive power of neural networks
- Developing machine-learning models based on logical characterisations