Image of finger pointin at a formula The research interests of the Programming Languages and Systems (PLAS) section span a broad range of areas, including theoretical foundations, languages for multicore and distributed computing, program analyses for testing and verification, advanced compilation techniques for parallel architectures, and the design of next-generation hardware accelerators.

The impact of our research is felt beyond academia and has led to start-up companies including Maxeler Technologies and Monoidics (the latter since acquired by Facebook) being formed.

Prof Wayne Luk, head of the PLAS section, is also director of our Centre for Doctoral Training on High Performance Embedded and Distributed Systems (HiPEDS), the aims of which intersect strongly with the section’s research goals.

Programming languages and software performance optimisation

Our aim is to design new languages and programming models that meet the often competing aims of:

  • allowing software to be expressed in a simple, elegant, modular and platform-agnostic manner, while
  • facilitating the generation of highly optimised low-level implementations that take advantage of the performance offered by modern concurrent and distributed platforms.

Examples of our efforts in this direction include multiparty session types for distributed computing, decoupled access/execute specifications for high performance computing, and lock inference techniques to support concurrent programming with atomic sections.

Software correctness, reliability and security

We lead the design of several static and dynamic program analysis techniques for sequential, concurrent and distributed software.

Methods pioneered by the PLAS section include testing and test generation through dynamic symbolic execution, proof techniques for concurrent algorithms and data structures based on local reasoning, automatic methods for analysing GPU kernels through symbolic program verification, and rigorous engineering of web applications through a certified JavaScript reference implementation.

We have collaborations with various industrial partners to apply analysis in order to help prevent software defects, and our analysis methods have been used to find bugs in very widely used software.

Hardware and accelerator architectures

A major focus of PLAS is on theory and practice of reconfigurable architectures and associated compilation techniques. This research includes:

  • architectures, design methods, languages, tools and models for customising computation, particularly those involving reconfigurable devices such as field-programmable gate arrays, and
  • their use in improving design efficiency and designer productivity for demanding applications, such as high-performance financial computing and embedded biomedical systems.

Tool support

We place a strong emphasis on building practical tools implementing our research ideas, for use by industry and to allow reproducibility of our research results. Key tools arising from the PLAS section and our international collaborators include:

  • Firedrake: a compiler for a domain-specific language for the finite element methods, that uses runtime code generation (via PyOP2) to deliver performance portability across CPUs and GPUs.
  • GPUVerify: data race analysis for GPU kernels (video)
  • JSCert: a mechanised semantics of the JavaScript programming language, and verified correct interpreter.
  • JuS: a general purpose analysis tool for JavaScript programs, which supports tricky features such as the notorious with statement
  • KLEE: automatic test case generation through symbolic execution
  • PyOP2: A framework for performance-portable parallel computations on unstructured meshes (video)
  • Scribble (JBoss)(GitHub): a language with tool support for describing and analysing application-level protocols among communicating systems


PhotoResearch Interests
  Photo of Dr Steffen van Bakel

Dr Steffen van Bakel

Functional Programming:Lambda Calculus, Term Rewriting Systems, Term Graph Rewriting Systems, Mobile Ambients, Systems Biology, Type systems: Sequent Calculus for Classical Logic, Curry Howard Isomorphism,Intersection type assignment, Polymorphic type assignment, Decidable systems, Type theory and theorem provers, Semantics: Filter models, Approximation models, Game theory and Abstract interpretation.
  Photo of Dr Cristian Cadar

Dr Cristian Cadar

Software Engineering, Computer Systems and Software Security, with a focus on building practical techniques for improving the reliability and security of software systems.

  Photo of Dr Cristiano Calcagno

Dr Cristiano Calcagno

Software Engineer at Facebook, builds tools which aid the development and certification of reliable software using lightweight formal methods.

  Photo of Prof John Darlington

Prof John Darlington

High Performance Apllied Computing, Internet Services and Economics and e-Science

  Photo of Dr Alastair Donaldson

Dr Alastair Donaldson (Joint Deputy Head of Section)

Formal verification techniques for multicore software. Software performance optimization for multicore processors

  Photo of Prof Sophia Drossopoulou

Prof Sophia Drossopoulou (Joint Deputy Head of Section)

Object Capability Policies, Concurrent Programming, Program Verification, Characterization of Program Evolution and Theorem Proving.

  Photo of Prof Susan Eisenbach

Prof Susan Eisenbach

Programming Languages, Concurrency and Testing.

  Photo of Prof Philippa Gardner

Prof Philippa Gardner

JavaScript, Concurrency and Resource Reasoning.

  Photo of Prof Chris Hankin

Prof Chris Hankin

Security, Program Analysis and  Programming Language Theory

 Photot of Preofessor Paul Kelly

Prof Paul Kelly

Languages, compilers, operating systems for parallel computing. Domain-specific tools and active libraries. Computer systems issues underlying performance. Software tools for portable parallel programming. Irregular and data-intensive applications. Applying a broad range of mathematical and theoretical ideas to computer systems problems. Performance evaluation, modelling and prediction. Caching, combining and randomisation in processors, multiprocessors, operating systems and wide-area networks and Language, linguistics, literature, literary theory

 Ben Livshits

Dr Ben Livshits

Security, Privacy, Program Analysis, Compilers, Software Engineering and Crowdsourcing.

 Photo of Professor Wayne Luk

Prof Wayne Luk (Head of Section)

Hardware and Architecture, Reconfigurable Computing, Design Automation

  Photo of Dr Sergio Maffeis

Dr Sergio Maffeis

Computer Security, Web Programming and Process Calculi

  Photo of Dr Oscar Mencer

Dr Oskar Mencer

Theory and practice, interaction of hardware and software systems. More specifically this includes domain specific representations of computation on the system level, the architecture level, and the bit-level, including programming methodologies that exploit spatial and temporal parallelism on all three levels with the objective of increasing computational speed while decreasing power consumption. My research interests include computer architecture from embedded processors to supercomputers, parallel programming and parallel architectures, computer arithmetic, custom computing, VLSI, CAD, compilers, dynamic optimization, algorithms and programming methodologies.

  Photo of Dr Iain Phillps

Dr Iain Phillips

Concurrency and reversibility, Mathematical Structures In Computer Science, Modelling of bonding with processes and events and Calculi for mobility.

  Photo of Prof Prof Nobuko Yoshida

Prof Nobuko Yoshida

Theoretical Computer Science

Summary of the table's contents