Mobile menu icon
Mobile menu icon Search iconSearch
Search type

Department of Computer Science


Verification of Efficient Algorithms in Isabelle/HOL

Primary supervisor

Additional supervisors

  • Lucas Cordeiro

Additional information

Contact admissions office

Other projects with the same supervisor

Funding

  • Competition Funded Project (Students Worldwide)

This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. Applications for this project are welcome from suitably qualified candidates worldwide. Funding may only be available to a limited set of nationalities and you should read the full department and project details for further information.

Project description

Correctness and efficiency of algorithms can be critical.
For example, model checkers and SAT-solvers employ complicated algorithms
which need to be highly optimized to be practically useful.
At the same time, bugs in these algorithms can have costly effects.

Such algorithms can be verified (ie. proved to be bug-free) using interactive theorem provers.
The state of the art however is to verify a rather abstract models
of the algorithm, which can either be implemented by hand (which again increases the risk of bugs),
or automatically extracted to rather inefficient functional code. Only a few efficient
implementations of algorithms have been verified, with considerable effort.

One promising technique for algorithm verification is stepwise refinement,
where an abstract model is refined towards an efficient implementation in many steps.
Each step can thereby focus on one idea of the algorithm or the implementation.
This natural separation of concerns makes the proofs more manageable and reusable.
In Isabelle/HOL, this approach has been used in the Isabelle Refinement Framework to
verify many nontrivial graph and automata algorithms, and whole model-checkers based
on these algorithms.

This project aims at continuing the development of an LLVM-backend for the Isabelle Refinement Framework,
which enables refinement down to LLVM-IR, which can then be compiled to very efficient machine code.
The current LLVM-backend is a shallow embedding of a very limited fragment of LLVM's semantics.
However, the shallow embedding inherently prevents some desired features like advanced control flow constructs
(e.g. break, exceptions). Moreover, the code-generator is non-trivial, and requires "hand-waving" correctness arguments.
For this reason, state of the art code-generators use a deeply embedded semantics, which does not have these problems.

The first goal of this PhD project is to develop a deeply embedded semantics of (a fragment of) LLVM-IR,
and the accompanying tools like code-extractor and verification condition generator.
Once this initial task is done, there are several possible continuations:
* Experiment on bottom-up verification, e.g., verify algorithms directly implemented in Isabelle-LLVM.
This may include implementation of abstraction methods (like Autocorres) to simplify the reasoning over fixed-size integers and memory.
It may also include the development of a verification friendly high-level language, which is compiled to LLVM.
* Extend the existing top-down refinement methods. Possible improvements are support of advanced control flow constructs, and more
automation with handling the refinement of arbitrary to fixed-size integers.
* Very probably, other interesting directions will be discovered during research on this topic.

Prerequisites:
Required: Background in interactive theorem provers and semantics of PLs.
Willingness to learn Isabelle/HOL. Much of the work will be implementing actual Isabelle/HOL theories!
Optional: Background in compilers, LLVM

Person specification

For information

Essential

Applicants will be required to evidence the following skills and qualifications.

  • This project requires mathematical engagement and ability substantially greater than for a typical Computer Science PhD. Give evidence for appropriate competence, as relevant to the project description.
  • You must be capable of performing at a very high level.
  • You must have a self-driven interest in uncovering and solving unknown problems and be able to work hard and creatively without constant supervision.

Desirable

Applicants will be required to evidence the following skills and qualifications.

  • You will possess determination (which is often more important than qualifications) although you'll need a good amount of both.
  • You will have good time management.

General

Applicants will be required to address the following.

  • Discuss your final year Undergraduate project work - and if appropriate your MSc project work.
  • How well does your previous study prepare you for undertaking Postgraduate Research?
  • Comment on your transcript/predicted degree marks, outlining both strong and weak points.
  • Why do you believe you are suitable for doing Postgraduate Research?