PLAS Research Interests
The Research Interests of the Programming Languages and Systems research group are listed by the interests of individual members.
I develop rigorous mathematical specifications, testing tools, and verification techniques for real-world concurrent systems, focusing on established interfaces (e.g. C, C++ and, OpenCL) and concrete testable artefacts (e.g. x86, Power, ARM CPUs, and Nvidia, AMD GPUs). My interests span a variety of complementary topics including: empirical testing of the behaviour of hardware and compilers, building formal models of parts of the system, the development of algorithms and data-structures that use fine-grained concurrency, and the verification of those pieces of concurrent code.
My research spans several areas, which include software engineering, concurrency and formal methods. I am interested in theories and tools for developing safe distributed systems. I am particularly interested in the formal foundations of service coordination and composition, business processes and their transactional behaviour, and the theory and application of behavioural types. Most recently, I have been working on the extension of Multiparty Session Types with logics to enable Design by Contract for concurrency, and the effective verification of real-timesystems.
My main research interests are in using mathematics and logic to ensure that computer programs do what they are supposed to do. This includes: calculi for program derivation; refinement; formal methods, in particular Z; viewpoint specification; security and cryptography. Recently I have also been looking at wider areas of security and privacy.
All my research interests are connected to programming and programming languages. I am interested in semantics and theoretical foundations of programming languages, type theory, program transformation, compiler construction, message-passing-based concurrency, programming tools, and how to write programs. I aim to support programmers in developing software more effectively. My favourite programming languages are functional languages, especially Haskell. Recently I became more interested in Erlang.
I am interested in software engineering for self-adaptive systems which involves the dynamic generation of processes and making systems and ensuring resilience. My background is in fault-tolerance and I am interested in designing architectural abstractions as well as validating dependable software architectures. Recently I have been investigating self-adaptive authorization for managing threats that come from inside an organisation.
I improve program analysis by reaching into the toolboxes of other
fields. Recently, for example, I sped up static analysis by using
machine learning, and I showed how runtime analysis can be grounded in the theory of automata over infinite alphabets.
My chief area of interest is dynamic memory management - this grew out of work on lazy functional programming languages and particularly their efficient implementation. My work spans from theoretical studies for example formalizing distributed reference counting and arguing its correctness to engineering concerns such as heat visualization and how to undertake rigorous and repeatable experiments in the context of benchmarking and particular memory management.
My main research interests are various flavours of term rewriting, e.g. infinitary rewriting, higher-order rewriting, as well as the first-order case. These cover the whole range from implementations, proving properties about them, to semantic models. In recent years I have been specialising on infinitary rewriting.
My interests range from high-level declarative programming to low-level assembly code. A reoccurring theme of my work is abstract interpretation in which all paths through a program are systematically examined so as automatically derive information for optimising a program for, say, time or energy. Abstract interpretation is also increasingly used to search a program for bugs, such as security holes, which another interest of mine. Recently I have been working on geometric algorithms, reverse engineering and malware.
My research focuses on understanding and describing computer hardware and programming languages to enable rigorous and trustworthy software verification. Precisely and unambiguously capturing the intricacies of these artifacts invariably requires the language of formal mathematics. To this end, I use techniques drawn from the interactive theorem proving and programming languages communities.
My main research interests are in functional programming, most recently to help people to write programs more effectively. In particular, I have been working on building refactoring tools for functional programs in Erlang and Haskell. I have also worked in reasoning and multimedia.
I believe many problems in software engineering can and can only be solved by better programming languages, and better ways of using them. A recurring theme of my research is to guarantee correctness of program properties through construction, reasoning and testing. Functional languages with many of their distinctive features are well suited for the task and have been the main target and carrier of my research. Some of my recent topics involve designing languages for bidirectional transformations and property-based testing.