Extracting Specifications of Runtime Behaviour
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.