IMDEA Software

IMDEA initiative

Home > Open Positions

Predicate Abstraction for Smart contracts

The IMDEA Software Institute invites applications for one visiting PhD position to work on the analysis of smart contracts via predicate abstraction. Enabledness predicate abstraction (EPA) is a method to abstract implementations of classes (in OO programming) or smart contracts to capture the evolution of the blockchain. However, currently these techniques filter away the information about the user interacting with the contract. In this work the intern will explore how to enrich current techniques with the ability to reason about the interactions of the different users with the contract and their relative powers.

In this project we aim to build a sophisticated system to analyze the execution of smart contracts to detect attacks, malicious users and their relations as well as other anomalies.

The ideal candidate should have a strong background in logic, automata formal languages, and formal methods in general. Experience with tools like Maude, K, TLA+ or Alloy is a plus.

Selected candidates will work with César Sánchez and an international team of graduate students and researchers.

Who should apply?

Candidates should have a MSc or BSc degree in computer science, mathematics, or a related discipline, be in the process of pursuing a PhD and have 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.

Working at IMDEA Software

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 5 months.

How to apply?

Applicants interested in the position should submit their application at using reference code 2023-04-phd-smartpa. Review of applications will begin immediately and close when positions are filled or on May 30th, 2023.

For enquiries about the position, please contact: cesar.sanchez (at)