© University of Kent - Contact | Feedback | Legal | Cookies
The University of Kent, Canterbury, Kent, CT2 7NZ, T +44 (0)1227 764000
|
|||
|
Programming Languages and Systems: PhD Studentships
This projects are merely suggestions and illustrate the broad themes of the research group. Potential research students are encouraged and welcome to produce their own suggestions in these research areas or other research areas in the field. All applicants are invited to contact the head of the group, Andy King, if they are considering an application.
Fully funded PhD studentships, which include maintenance fees at £12,300, are available from October 2009.
Architecting Resilience in Self-organising Systems
Contact: Dr. Rogerio de Lemos
Self-organising systems are those systems where there is no explicit central control either internal or external. In other words, these systems are decentralized in nature, implying that access to global information is limited or impossible, hence adaptation should be based on interactions occur locally (among neighbours) and based on local information. On other hand, resilience is related to the persistence of service delivery that can justifiably be trusted, when facing changes. There are two issues that need to be considered in resilient system: first, it is the ability of the system to provide resilience, and second, it is the ability to justify the provided resilience. This project aims to define an architectural abstraction for supporting resilience in self-organising systems.
Autonomy in the Presence of Failures
Contact: Dr. Rogerio de Lemos
The level of autonomy in embodied systems is essentially constrained by the intent of the system and the resources available to achieve that intent, thus the reasoning about failures in system resources should be an integral part in system design. In other words, the provision of autonomy should rely on how the system is built in terms of its hardware and software components, and how these can be exploited for the continue delivery of system services despite the presence of failures. The basis of the proposed approach is the definition of architectural abstractions that support adaptability, facilitate the handling of faults, and promote autonomy. These abstractions contain well-defined interfaces that express the different roles in which an abstraction might be involved, promote error confinement, and enforce crash-failure semantics when enough resources are available or employ dynamic recovering techniques for exploiting inherent system redundancies.
CRS Compilation via Nested Types
Contact: Dr. Stefan Kahrs
Combinatory reduction systems are fairly hard to implement correctly and efficiently, because a simple implementation will be inefficient because it uses repeated renamings of bound variables (de Bruin index adjustments), while an efficient one has a hard task to get the renamings right. However, the de Bruin indices can be expressed through nested types too which would guarantee (a large part) of the correctness of the renaming. The task is to bring these two worlds together.
Checking out Monte Carlo
Contact: Dr. Eerke Boiten
Monte Carlo algorithms are probabilistic algorithms which return the right answer most of the time. This project uses recently defined theories of correctness of probabilistic algorithms, and of ``most-of-the-time" correctness, in order to check correctness of Monte Carlo algorithms. This will incorporate analysis of the algorithms' running time in a suitable way, and generate ideas on how to construct Monte Carlo algorithms from problem specifications.
Failure Handling in Concurrent Systems
Contact: Dr. Fred Barnes
Projects: RMoX
Software-based protection in many modern languages is done using a try-except-finally based exception handling mechanism, that more or less provides an alternative return path between procedures. For some, particularly concurrent and process-oriented languages, this approach is sufficient for handling sequential code, but is unsuited for handling failure in networks of concurrent and communicating processes.
Research in this area will investigate existing approaches towards failure handling in software systems, both practical and theoretical, concentrating on failure handling in concurrent systems. Open questions include: given a network of communicating parallel processes in which one component fails, how should the components with which it is communicating be dealt with? The results of research in this area will include new or modified theories about the operation of concurrent systems, language bindings for providing a concise programmer interface and run-time support for the implementation of these.
Implementation of Optimal Reduction
Contact: Dr. Stefan Kahrs
20 years ago Lamping came up with the idea of optimal reduction for the lambda-calculus, supported by a graph-like structure that would make even fewer reductions than lazy evaluation. An implementation as a proof of concept was done in Bologna some years later, but there has been no serious attempts at replacing real-world functional programming implementations with a system based on these ideas.
Inductive Programming for Better Testing
Contact: Professor Simon Thompson
How can you tell how good a set of tests you have? One answer is to look at how much of your program they "cover", or at how they fail when you mutate the program a little. Another approach, which we began to explore in the ProTest project on property-based testing, is whether we can infer a program from the set of tests, and assess whether or not it has similar behaviour to the existing program.
In ProTest we concentrated on state-based systems; in this project the idea would be to look at tests for pure functional programs - written in Haskell - and object-oriented programs - written in Java - and to extract programs from the tests to compare with the originals. More information about the ProTest work can be found here and here.
Practical Formal Verification of Concurrent Systems
Contact: Dr. Fred Barnes
Projects: RMoX
Much of the concurrency research undertaken at the University of Kent relates to the process-oriented abstraction of layered networks of communicating parallel processes. In these systems, thousands to millions of individual concurrent processes communicate with each other in well-defined ways to provide an overall functionality. Benefits of this approach include the ability to scale across single chips, multicore processes and distributed systems, as well as compositional and scalable approach to building these systems. Unlike traditional sequential systems, networks of concurrent processes can deadlock or livelock, errors arising from incorrect communication between components.
Research in this area will investigate practical approaches for the formal verification of concurrent systems. Some work in this area has already been undertaken at Kent as part of the RMoX project. Specifically, the automatic generation of CSP models of process behaviour from occam-pi source code, models which can then be checked against specifications in model-checkers such as FDR2. However, this is only a start and there are several unanswered questions, such as how to handle the dynamic reconfiguration of process networks. Within the context of RMoX, additional concerns include verification of low-level code code, e.g. to ensure that device-drivers interact with hardware devices in the intended (specified) way. This research project will broadly investigate these issues.
Programs as Matrices
Contact: Dr. Andy King
Programs are complex and therefore it is difficult to get computers to reason about other programs automatically to check that they are correct. It is not even straightforward to compose two methods calls: this is needed to work out what is the combined effect of two method calls do when one call follows another.
On the other hand, matrices are simple, and they can be composed and easily stored and manipulated by computer programs. The project will take the primitive operations that arise in a program, such as assignment, if-then-else, etc and model these operations as matrices. Then the matrices will be composed to model method calls and the program as a whole. The studentship will investigate the scalability of this technique and apply it to finding bugs in programs.
Refactoring Dependently-Typed Programs
Contact: Professor Simon Thompson
There is a growing interest in dependently-typed functional programming, in systems like Agda as well as in theorem provers such as Coq. In a dependently-type program, the type of the result of a function can depend on the value of a function argument, so that types can give a much closer description of the behaviour of a function, and indeed in the most complex case, represent the full specification of a function.
One of the big problems that emerges in using a dependently-typed system is its sensitivity to the way that data are represented. While abstractly lists of a certain length are equivalent to finite maps of a particular kind, it's often useful to be able to convert between data representations in developing a system. This is a challenging use case for refactoring of such programs, and this thesis project aims to build a tool to support a portfolio of refactorings for dependent types and programs using them.
The Kent functional programming team have world-leading expertise in building the refactoring tools Wrangler for Erlang and HaRe for Haskell; we've also been thinking about dependently-typed programming for twenty years.
Reverse Engineering
Contact: Dr. Andy King
Reverse Engineering is the process of taking a software artifact, such as a binary, and figuring out what it does. Reversing is important in the security industry where security engineers frequently have to inspect binaries when searching for security holes. This project will develop tooling not for reversing a binary to, say, a C program or even an intermediate language. Rather the project will develop tools that explain what a binary does by annotating it with information that details the values register might store. This will be achieved, not by directly executing the binary (since the binary may be malicious) but rather by following all paths through the binary. In this way, it is potentially possible to work out the values that registers will possibly store at each point in the binary. The studentship will develop this idea and apply it to develop tools for supporting security engineers.
Sound Trusting for Tracing Haskell Programs
Contact: Dr. Olaf Chitil
Hat (www.haskell.org/hat) is a sophisticated tool for locating faults in Haskell programs. Hat consists of a trace generation system plus various tools for viewing a trace. Tracing every detailed step of a longer running computation is practically infeasible, the trace becomes too big and most of it will never be needed anyway. Instead, only the computations of some program parts are traced whereas standard libraries and other parts are trusted to be correct and hence are not traced. Traced code can call trusted code and vice versa, but the current implementation of this interaction is crude, leaving gaps in the trace and tracing some computations unnecessarily. The aim of this project is to develop a scheme for trusting that will be implemented and will be proven to be sound with respect to various uses of the trace, especially algorithmic debugging.
Static Contracts for Communicating Erlang Processes
Contact: Dr. Olaf Chitil
Erlang is a concurrent functional programming language designed by Ericsson with dynamic process creation and asynchronous message passing. Type systems have been defined on top of the dynamically typed Erlang language, but these concentrate on the traditional, non-concurrent aspects of the language. The aim of the research project is first to define a language for expressing properties of process creation and communication, for example communication protocols. These properties are expressed as contracts that state which program part to blame if the property does not hold. These contracts shall prevent many concurrency-related runtime errors but still allow common Erlang programming patterns. The second challenge is to devise algorithms for statically checking these contracts. The project will build on a wide area of previous research on type systems, dynamic and static contracts for functional languages and session types.