Detailed below is a list of selected research projects of Group Members. Smaller projects with a budget lower than £50k are not listed here.
Current Grants
- Grad4HOProb: Graded Modal types for Quantitative Analysis of Higher-Order Probabilistic programs, Vineet Rajani, Dominic Orchard, ARIA, 2024-2025, £226K
- MEBI: Mechanised Bisimilarities and Behavioural-typed Processes, David Castro-Perez, ISPF, 2024-2025, £162,324
- Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT), Mark Barry, EPSRC, 2023-2027, £374,698
- TYPDSEC: Type-based information declassification and its secure compilation, Vineet Rajani, EPSRC, 2023-2025, £160K
- Transparent pointer safety: Rust to Lua to OS Components, Mark Batty, Simon Cooksey, Michael Vollmer, 2022-2025, £494,770
- FastStart: Fast SingleTruth Language Runtimes, Stefan Marr, 2021-2024, £120,003
- Session Types for Reliable Distributed Systems (STARDUST), Laura Bocchi, David Castro-Perez, Simon Thompson, EPSRC, 2020-2025, £555,120
Previous Grants
- CapC: Capability C semantics, tools and reasoning, Mark Batty and Stephen Kell, August 2020-July 2024, £485,168
- CaMELot: Catching and Mitigating Event-Loop Concurrency Issues, Stefan Marr, April 2021-March 2023, £209,756
- Verifying Resource-like Data Use in Programs via Types, Dominic Orchard, July 2020-Juen 2023, £229,328
- Generalised static checking for type and bounds errors, Stephen Kell, September 2019-March 2023, NCSC, £75,000.
- Symbolic Computation for Mainstream Verification, Andy King and Budi Arief, April 2021-March 2022, £77,500
- Building Verified Applications in CakeML, Scott Owens, October 2018 – September 2021, NCSC £74,000
- Specification and Verification of C++ Data Structure Libraries, Mark Batty, October 2018 – September 2021, NCSC £82,000
- Verifiably Correct Transactional Memory, Scott Owens and Mark Batty, September 2018 – August 2021, EPSRC £82,900
- Behavioural API’s, Laura Bocchi, March 2018 – April 2022, EC £41,000
- Fixing the thin-air problem: ISO dissemination, Mark Batty, October 2019-September 2020
- Trustworthy Software for Nuclear Arms Control, Aziem Chawdhary and Andy King, May 2018-August 2019, NCSC £72,000
- Compositional, dependency-aware C++ concurrency, Mark Batty, April 2018-March 2020, EPSRC £122,126
- Fast Run-time Verification via Machine Learning, Radu Grigore, January 2018 – December 2019, EPSRC £101,000
- The Rise and Fall of COOP, Andy King, March 2017 – March 2021, GCHQ £121,000
- Time-sensitive protocol design and implementation, Laura Bocchi, 2016-2019, EPSRC, £101,196
- Trustworthy refactoring, Simon Thompson and Scott Owens, September 2016 – March 2020, EPSRC £728,766
- Marlowe: Domain-specific language for the design of smart-contracts over cryptocurrencies, Simon Thompson, September 2016 – May 2019, IOHK £207,400
- Vulnerability Discovery using Abduction and Interpolation, Aziem Chawdhary and Andy King, August 2016 – August 2019, EPSRC, £199,130
- Testing Techniques for Functional Programming Languages, Meng Wang, March 2016-Feb 2018, Royal Society International Exchange, £10,000
- CGrail: unified, optimisable and formally specified C concurrency, Mark Batty, Jan 2016-December 2020, REng Research Fellowship, £526,646
- Heterogeneous memory model study, Mark Batty, December 2015-March 2016, GCHQ, £19,600
- CamFort: Automated evolution and verification of computational science models, Dominic Orchard (Co-investigator), July 2015-August 2018, EPSRC, £542,082
- Verifying current algorithms on Weak Memory Models, Scott Owens, May 2015-October 2018, EPSRC, £285,988
- Relaxed Memory Model Design for Theory and Practice, Scott Owens, Jan 2014-Jan 2016, EPSRC, £98,538
- Se-Ma-Match: Semantic Malware Matching, Andy King, October 2013-October 2016, EPSRC, £245,525
- Compositional Security Analysis for Binaries, Andy King, August 2013-September 2017, EPSRC, £228,823
- RELEASE: A High-Level Paradigm for Reliable Large-scale Server Software, October 2011-September 2014, Simon Thompson, EU STREP, £310,000