Application Form
Post-Doctoral Researcher (Formalising Specifications for Software Verification)

JobRef: 23265
  • Accepted file types: pdf, Max. file size: 12 MB.
  • Accepted file types: pdf, Max. file size: 2 MB.

Post-Doctoral Researcher (Formalising Specifications for Software Verification)

Level:Postdoctoral Researcher
POSTED:May 27, 2024
LOCATION:Maynooth University
Duration:Temporary Contract to 31/1/26
Reports to:Rosemary Monahan <[email protected]>
Salary:Postdoctoral Researcher (2023) Salary Scale: €42,783 - €49,117 p.a. (6 points); Senior Postdoctoral Researcher (2023) Salary Scale: €50,540 (1 point)
Closing Date:June 9, 2024

Please note the below is a shortened version of the full job specification. For more details please refer to the full Job Description document, which can be downloaded by clicking on the ‘Download full job spec’ button above.

The Role 

Maynooth University is committed to a strategy in which the primary University goals of excellent  research and scholarship and outstanding education are interlinked and equally valued.  

We are seeking an energetic and enthusiastic postdoctoral researcher to work on techniques for  formalising specifications for software verification. Our overall goal in this research, is to provide for the  automatic generation of formal specifications, and to support the traceability of the requirements from  the initial software design stage through the systems implementation and verification

The Project  

VERIFAI: Traceability and Verification of natural-language requirements 

To verify the correctness and reliability of safety critical software, we express safety properties of the  system as a collection of formal specifications that are unambiguous and that can be reasoned about  mathematically. Verification of these formal specifications is achieved through methods such as  deductive verification, model checking and runtime verification.  

A major burden in this process is the generation of the formal specifications. The requirements elicitation  process starts with natural language requirements which are often ambiguous, leading to incorrect  properties of a system being specified, and systems that are under-specified due to the assumptions of  the domain knowledge. Furthermore, traceability from the original system requirements through to the  properties of the implemented system is often missing. With the use of machine learning in systems  development, requirements traceability becomes even more crucial: as a software system learns, we  must ensure that safety properties identified at the design stage are maintained in the final system; as  the system evolves we must track the changes to the original software requirements, to give a better  understanding of the behaviour of the AI; and we must monitor the impact of the training data used, to  direct learning so that safety properties are maintained by the system. 

This project will address these challenges through providing support for the automatic generation of the  formal specifications, and the traceability of the requirements from the initial software design stage through the systems implementation and verification. In this way we can ensure that when a system is  implemented, we not only build the correct system, but we also build the system correctly. In addition,  if an error occurs in the expected behaviour of the system, we can trace to where and when the source  of the violation occurs. Approaches which will be explored as part of this project include Natural  Language Processing, use of ontologies to describe the software systems domain, reuse of existing  software artefacts from similar systems (e.g. through similarity –based), and large language models to  identify and declare the specification as well as use of artificial intelligence to guide the process.  

Apply Now

Other Positions