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