Programming Languages and Systems
The Programming Languages and Systems (PLAS) research group researches both practical and theoretical aspects of program design and system building.
Our work in languages encompasses programming across a broad range of paradigms: concurrent, imperative, functional, logic and object-oriented.
These interests are complemented by architectures and systems research in intrusion detection, mobile and distributed systems.
Our work is linked by shared interests in semantics, verification and implementation. Common aspirations of the PLAS group are to develop techniques and tools for program manipulation, ensure program correctness, and improve the reliability and security of programs.
The group focuses on the specification, design and implementation of computer systems, from the very large to the very small, and characterised by the interplay between theory and practice. It has three main research themes: verification and dependability; memory management; and program development.
Verification and dependability
Stefan Kahrs has developed foundational proof techniques for rewriting, which in turn underpin work on program correctness. Eerke Boiten is concerned with the relation between state-based and behavioural specification methods.
Andy King has developed techniques that apply abstraction to automatically diagnose flaws in existing programs. Rogério de Lemos has applied verification at the architectural specification level to assure dependability.
Mark Batty has developed rigorous specifications for the C and C++ memory model and OpenCL. Scott Owens has co-developed a verified implementation of ML. Radu Grigore has developed data-structures for runtime verification.
Professor Richard Jones' work has focused on garbage collection on multicore systems, including understanding the overheads placed by concurrent applications on runtime systems, reducing memory overheads in real-time systems, and exploring locality.
Professor Simon Thompson has developed the Wrangler refactoring tool for Erlang and developed techniques for users to
define new refactorings. Olaf Chitil has explored how contracts - expressing requirements for functional programs - interact with laziness.
Meng Wang has designed languages for bidirectional transformations and property-based testing.
Laura Bocchi has extended session types with logics to enable design by contract for concurrency.
Interested in postgraduate study?
We recruit new PhD and MSc research students every year. We offer a research environment of international quality and an impressive support package for research students.
- Time-sensitive protocol design and implementation, Laura Bocchi,
December 2016-November 2018, EPSRC, £101,196
- Trustworthy refactoring, Simon Thompson and Scott Owens, September 2016—March 2020, EPSRC £*728,766
- Vulnerability Discovery using Abduction and Interpolation, Andy King and Aziem Chawdhary (Research Co-Investigator), August 2016 – March 2018, 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 (Research Co-investigator), July 2015-August 2018, EPSRC, £20,000
- 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