The overall goal of the project is the study of extensions and algorithms based on temporal logic in two important application domains.
One is the analysis of industrial requirements for critical systems, which oftern can be modeled using temporal logic. It is crucial that problems in the requirement phase are uncovered early, and several of these problems can be reduced to realizability of safety LTL specifications. The main goal of this part is to improve the scalability of realizability by studying decomposition algorithms.
The second application area is the offchain dynamic analysis of blockchain and smart contract executions. Here the temporal logic is the basis of a query language to analyze executions, extract violations of desirable behaviors and produce explanations. Here the challenge is to extend the logic with capabilities to reason about the users of the blockchain and their powers, alternative execution traces and the data produced and token exchanged. The algorithms in this case are runtime verification algorithms that will be implemented on top of blockchain indexers.
Applications are invited to apply for a PhD position at the IMDEA Software Institute, Madrid, Spain.
Selected candidates will work with César Sánchez and an international team of graduate students and researchers focusing on Blockchain reliability.
Candidates should have an excellent MSc or BSc degree (or be close to complete one) in computer science, mathematics, or a related discipline, with an interest in the above area, and a strong commitment to research. Proven top programming skills as well as ability to understand and develop algorithms are required. Good teamwork and communication skills, including excellent spoken and written English are also required.
The position is based in Madrid, Spain, where the IMDEA Software Institute is situated. The institute provides for travel expenses and an internationally competitive stipend. The working language at the institute is English.
The duration of the position will be 4 years.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2021-12-phd-specs. Review of applications will begin immediately and close when positions are filled or on January 15th, 2022.
For enquiries about the position, please contact:
