Extracting Specifications of Runtime Behaviour

Primary supervisor

Contact admissions office


  • 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

Formal specifications of program behaviour are generally difficult to write but can be used in a number of useful tasks, not least in (compositional) program verification. Specification mining is a field that aims to extract specifications from programs and one particularly interesting subfield is that of dynamic specification mining that extracts temporal specifications from program traces. Such an approach has two main advantages: firstly, the source code is not required, and secondly, only frequent or common behaviours are considered. When exploring such methods there are two main variations in setting; firstly what data is available i.e. can a system be queried to extract new traces, and secondly, what kind of specification is being extracted i.e. does it incorporate real-time information, data-dependencies etc. Much of this space is yet to be explored and there is a lack of a unifying underlying theory.

This project will look at the problem of extracting highly expressive specifications from program traces. The exact focus of the project will depend on the student???s interests, it could focus on developing theoretical foundations, it could be centered around a particular application, picking up on domain-specific requirements, or it could be more programming intensive with a focus on tool development and experimental analysis.

The interested student should have an interest in formal methods and program verification and have reasonable programming skills.

▲ Up to the top