Research Groups

A fully-funded, PhD position is now available at the AI research group

This fully-funded position will aim to improve both the modelling capabilities and the solving performance when confronting Automated Planning problems. We seek motivated candidates with a strong background in Computer Science, with excellent programming skills and some previous knowledge and experience in solving combinatorial optimisation problems.

Please take a look at the instructions on on how to apply.

The University of St Andrews is the top university in Scotland and second in the UK in The Times and Sunday Times Good University Guide 2023. Last year St Andrews was ranked number one in the UK, the first time in the near 30-year history of the Guide, or any UK ranking, that any university has been placed above those of Oxford and Cambridge.

If you are interested in either knowing more or have any informal enquiry, please do get in touch with Joan Espasa Arxer via email: jea20@st-andrews.ac.uk

The deadline for applications is the 1st of March 2023. 

Fully funded PhD scholarship: Trustworthy Refactoring Tools for Haskell Programs

Supervisor: Dr Christopher Brown

Proposal and Context

Software is large and complex. Ubiquitous systems, such as weather forecasting, medical imaging, advanced AI and big-data processing are extremely expensive and time-consuming for software companies to produce. Moreover, they often comprise many subtle bugs that can have disastrous consequences, are difficult to find, and difficult or impossible to fix. What developers need are specialised software refactoring tools that help them develop these important and complex systems in a safe and semi-automated way, reducing developer time, human error and overall increasing productivity, saving companies and customers money, and providing robust, safe, systems that have been developed in a responsible and trustworthy way.

Refactoring is the process of changing the structure of software without changing what it does: in effect, refactoring is about helping the programmer re-purpose their code to make it more understandable, accessible, or amenable to further change in the program’s design. It is often a process that developers use on a daily basis by manually changing code to reflect an API change, re-purposing methods, eliminating duplicated code, remaining variable parameters and function names, generalising functions, etc.  However, this process is rather tedious and cumbersome to apply manually: effecting a structural change that could potentially affect millions of lines of code across thousands of files is inevitably error – prone.

The advent of refactoring tool-support provides developers with automated transformations that they can apply to their code base, usually through an existing IDE interface. Refactoring tools, on the other hand, provide a way to apply refactorings across an entire code base in a semi-automatic way: they rely on the user to make certain choices about which refactorings to perform but are automatic in their underlying machinery. This automated underlying machinery means that both simple and complex refactorings can be applied to large code bases comprising thousands of files and millions of lines of code instantly.

However, automated tools are prone to bugs. This has the potentially disastrous consequence of a refactoring tool refactoring a program into one that contains subtle bugs or changes in behaviour. Despite the obvious implication that this will refactor software to contain, perhaps, subtle and difficult-to-spot bugs, it also erodes developers’ confidence in using refactoring —and general software tools— in general. Furthermore, a refactoring that introduces errors or is not trustworthy requires the programmer to inspect the transformed code, therefore taking out the benefit of using an automated tool in the first place. The problem is also amplified in that refactoring tools are extremely cumbersome, laborious and difficult in themselves to implement, especially over large programming languages, such as Haskell. This makes the refactorings deployed in such tools limited, both in number and applicability.

What is needed is to answer the following research questions:

  1. How can we provide an automated approach of implementing refactoring tools, via compositionality and proof search?
  2. How can we have the means to generate new refactorings easily that are safe and trusted by the developers that require them?
  3. How can we provide a means to generate soundness proofs that the refactorings are safe and verified, in an automated way?

Exploratory Ideas

The PhD will be exploratory in nature. Here are some ideas for research directions to investigate as part of the PhD:

  1. Formally characterise a number of refactorings for Haskell and prove properties of their general soundness.
  2. Develop a fully verified refactoring tool that encodes general soundness proofs as part of its implementation using e.g., Dependent Types for the full Haskell standard.
  3. Model a fully verified static and functional semantics for Haskell using e.g., Dependent Types.
  4. Provide a fully generalised theory of the formalisation of refactoring tools for e.g., Haskell.
  5. Provide an automated technique to find refactorings and proofs of refactorings, via e.g., proof search and compositionality of sub-proofs.
  6. Evaluate the applicability of the approach on a number of use-cases and domains, from a variety of languages, across a different number of verticals.

Supervisor and Background

The PhD project is to be supervised by Dr Christopher Brown, a lecturer in the school of computer science who has over 18 years of experience working in the field of refactoring, program transformation and functional programming. Dr Brown contributed to the original HaRe (Haskell Refactorer) system, developed at the university of Kent, and has since developed a number of new refactoring tools for a variety of languages, including Haskell, Erlang and C/C++ for introducing and tuning parallel programs. Dr Brown also works in the field of formal semantics, with prior work on formalising refactorings and using types to reason about e.g., extra functional properties of imperative systems for embedded languages.

The PhD project fits directly with the research vision of the supervisor, who is also working on building refactoring tools for dependently typed languages, such as Idris and Pi-Forall.

The Programming Languages Research Group

The Programming Languages Research Group has a long history in functional programming and type theory. This project would directly fit with the group’s general vision of:

  1. Making programming languages more accessible to experienced and inexperienced programmers alike.
  2. Providing tool-support to make programming more accessible to inexperienced programmers.
  3. Using types to formalise general soundness of programming language properties and semantics.
  4. Providing verified refactoring tooling for functional programs.

To apply

Informal inquiries can be directed to Chris Brown. Formal applications can be made through the School’s postgraduate research portal.

The deadline for applications is 1 March 2023.

Congratulations Rosa!

Congratulations to Rosa Filgueira who has been awarded with the UK Young Academy (UKYA) membership

The UK Young Academy’s first cohort brings together members from across academia, charity organisations and the private sector, to galvanise their skills, knowledge, and experience to find innovative solutions to the challenges facing societies now and in the future.

PhD success for a former graduate

Last month Professor Simon Dobson was invited to be on the PhD examining committee for Indushree Banerjee at TU Delft.

PhD examining committee, paranymphs, and family

She passed with flying colours, for her thesis on ad hoc network protocols for use in disaster recovery situations. The protocol is designed around a very strong model of social justice and equality, working on low-power mobile devices and operating so as to conserve power reserves and device lifetime over the important 48-hour initial period of disaster relief.

Indushree did her MSc in St Andrews ten years ago, which gives us the opportunity for a couple of before-and-after photographs.

Simon and Indushree, MSc graduation 2012 Simon and Indushree, PhD graduation 2022

Neither of them seem to have changed all that much, apart from Simon having gone “Full Gandalf” during lockdown.

Indushree is now doing a postdoc in Delft, focusing on technology applied to  wildlife conservation and ecology. We’re hoping to get her over for a seminar in the new year.

Clouded | Uncovering The Culture Of Cloud

Congratulations to Blesson Varghese who features in a newly released documentary in collaboration with Hewlett Packard Enterprise and VMWare.

An original film that is uncovering the realities of cloud technology and its effects on both business and society. Many have grown confused with our relationship with a rapidly expanding cloud market, others are reflecting on their strategies. The question is, when did cloud become so ‘Clouded’.

Clouded confronts some of the uncomfortable truths that exist in today’s cloud culture. This is a journey of discovery that uncovers topics which undoubtedly require further thought by governments, enterprise businesses and technology executives.

The full documentary can be watched at https://www.consciouslyhybrid.com

Research Away Day October 2022

Thanks to everyone who attended the school Research away day. The day was very informative and lots of ideas were created.

It was lovely to meet our Ukrainian Visiting Academics Maryna Novozhylova and Olga Chub.

We would also like to thank our guests, Ricky Shek from careers, Kirsty Ross from RIS,  Adeel Shafi and Jayshree Johnstone from business development.

PhD Viva Success: Chawanangwa Lupafya

Please join me in congratulating Chawanangwa Lupafya, who has just passed his PhD viva subject to minor corrections.

Chawanangwa is supervised by Dr Dharini Balasubramaniam.

Special thanks to Dr Ruth Hoffman for serving as internal examiner and  Dr Rami Bahsoon from the University of Birmingham for serving as the external examiner

 

PhD Viva Success: Yasir Alguwaifli

Please join me in congratulating Yasir Alguwaifli, who has just passed his PhD viva subject to minor corrections.

Yasir, who is supervised by Christopher Brown, has provided his thesis abstract below.

Thanks to Özgür Akgün for serving as internal examiner and Prof Christoph Kessler from Linköping University for serving as the external examiner.

Controlling energy consumption has always been a necessity in many computing contexts as the resources that provide said energy is limited, be it a battery supplying power to an Single Board Computer (SBC)/System-on-a-Chip (SoC), an embedded system, a drone, a phone, or another low/limited energy device, or a large cluster of machines that process extensive computations requiring multiple resources, such as a Non-Uniform Memory Access (NUMA) system. The need to accurately predict the energy consumption of such devices is crucial in many fields. Furthermore, different types of languages, e.g. Haskell and C/C++, exhibit different behavioural properties, such as strict vs. lazy evaluation, garbage collection vs. manual memory management, and different parallel runtime behaviours. In addition most software developers do not write software with energy consumption as a goal, this is mostly due to the lack of generalised tooling to help them optimise and predict energy consumption of their software. Therefore, the need to predict energy consumption in a generalised way for different types of languages that do not rely on specific program properties is needed. We construct several statistical models based on parallel benchmarks using regression modelling such as Non-negative Least Squares (NNLS), Random Forests, and Lasso and Elastic-Net Regularized Generalized Linear Models (GLMNET) from two different programming paradigms, namely Haskell and C/C++. Furthermore, the assessment of the statistical models is made over a complete set of benchmarks that behave similarly in both Haskell and C/C++. In addition to assessing the statistical models, we develop meta-heuristic algorithms to predict the energy consumed in parallel benchmarks from Haskell’s Nofib and C/C++’s Princeton Application Repository for Shared-Memory Computers (PARSEC) suites for a range of implementations in PThreads, OpenMP and Intel’s Threading Building Blocks (TBB). The results show that benchmarks with high scalability and performance in parallel execution can have their energy consumption predicted and even optimised by selecting the best configuration for the desired results. We also observe that even in degraded performance benchmarks, high core count execution can still be predicted to the nearest configuration to produce the lowest energy sample. Additionally, the meta-heuristic technique can be employed using a language- and architecture-agnostic approach to energy consumption prediction rather than requiring hand-tuned models for specific architectures and/or benchmarks. Although meta-heuristic sampling provided acceptable levels of accuracy, the combination of the statistical model with the meta-heuristic algorithms proved to be challenging to optimise. Except for low to medium accuracy levels for the Genetic algorithm, combining meta-heuristics demonstrated limited to poor accuracy.