Program Analysis Research
Our program analysis research focuses on verifying concurrent programs through various methods.
Our research
We use formal verification techniques to ensure correctness and security in software programs. We use a variety of methods for program analysis, including:
- summary-based approaches
- rely-guarantee reasoning
- concurrent separation logic
- type systems
- bounded model checking
- abstract interpretation
- automated testing
Our Advanced Model-Based Engineering and Reasoning (AMBER) group leads our program analysis research.
TRUSTED
- Project: TRUSTED: Security Summaries for Secure Software Development
- Researcher: Dr Narges Khakpour
- Funder: EPSRC
- Funding amount: £919k
- Duration: 2023 – 2026
- Website: trusted-ssd.github.io/TRUSTED/
This EPSRC funded project aims to protect software systems against supply chain attacks, by developing:
- formal static analysis techniques
- tools for secure software development
Separation and interference
- Project: Separation and Interference
- Researcher: Professor Cliff Jones
- Funder: Leverhulme
- Funding amount: £138k
- Duration: 2019 – 2023
This project tackled recording the scientific history of research on formalisms for specifying and developing software that employs concurrency. The Leverhulme Foundation funding was crucial because of the cross-disciplinary nature of such work.
Taming concurrency
- Project: Taming Concurrency
- Researcher: Professor Cliff Jones
- Funder: EPSRC
- Funding amount: £643k
- Duration: 2013 – 2019
Jones's research on "rely/guarantee methods" continues to stimulate many researchers. This project enabled closer collaboration with research on "concurrent separation logic" which is the other widely used approach for concurrency (with a focus on heap variables).
AI4FM
- Project: AI4FM
- Researcher: Professor Cliff Jones
- Funder: EPSRC
- Funding amount: £467k
- Duration: 2010 – 2014
This project explored ways in which AI approaches could help the formal development of software. Specifically, it took the approach of mining proof attempts (not just finished proofs) to detect patterns in attacks on particular applications. It was, for example, found that once a few key lemmas were established that related to specific data structures and functions, they made automatic proof far more practical.
