PhD: Formal Verification Techniques for Reversible Languages — DC3

We welcome applications from all qualified candidates regardless of nationality, ethnic origin, gender, sexual orientation, religion or belief, disability, or age. Selection is open, transparent, and merit-based.

About the E-CoRe project

E-CoRe (Energy-efficient Computing via Reversibility) is a Horizon Europe project funded under the Marie Skłodowska-Curie Actions Doctoral Networks. The project advances the science and practice of reversible computing for a sustainable digital future, training the next generation of experts to make computing sustainable. Energy is a main concern in society: IT accounts for an estimated 10% of global energy consumption. Reversible computing avoids the fundamental energy lower bound imposed by Landauer's principle by discarding no information. E-CoRe aims to set the stage for the Reversible Computing revolution by forming a community of experts who will improve and popularize reversible languages, algorithms and architectures — in energy-intensive applications such as machine learning, blockchains and drones. For the full project description, see: Project Description.

About the environment: CNRS / Université Côte d'Azur

The Université Côte d'Azur (UCA) brings together the major players in higher education and research on the French Riviera. The CNRS laboratory I3S has strong expertise in formal methods, concurrency, and verification. Nice and Sophia Antipolis offer a unique Mediterranean setting with a dynamic tech ecosystem and excellent quality of life.

About the position topic

This doctoral position is part of Work Package 1: Reversible Programming Languages. The successful candidate will work on Formal Verification Techniques for Reversible Languages.

The DC will investigate new logics for truly concurrent systems with specific operators for causality, consistency and reversible modalities. Model checking will be complemented by runtime monitoring through types. For concurrent reversible processes, the DC will investigate the development of appropriate session type disciplines.

For the full topic description, objectives, expected results, and planned secondments, see: Topic: Formal Verification Techniques for Reversible Languages.

MSCA Doctoral Candidate eligibility criteria

To be eligible, you must satisfy all of the following conditions at the date of recruitment:

1. Doctoral candidate status: You must not hold a doctoral degree. Researchers who have successfully defended their doctoral thesis but have not yet formally been awarded the doctoral degree are not eligible.
2. Mobility rule: You must not have resided or carried out your main activity (work, studies, etc.) in France for more than 12 months in the 36 months immediately before the recruitment date. Compulsory national service, short stays such as holidays, and time spent as part of a procedure for obtaining refugee status under the Geneva Convention are not taken into account.
3. Enrolment: You must be enrolled in a doctoral programme at the host institution during the project.
4. Nationality: Researchers of any nationality may apply.

Other requirements

• Master's degree (or equivalent) in computer science, mathematics, electrical engineering, or a closely related field, obtained by the recruitment date.
• Strong academic record and motivation for doctoral research.
• Proficiency in written and spoken English.
• Ability to work in an international, collaborative environment.
• Willingness to undertake secondments to other project partners as specified in the topic description.

Remuneration

The remuneration is based on the MSCA Doctoral Network researcher allowances:

• Living allowance: 4,010 € per month (adjusted by country coefficient)
• Mobility allowance: 710 € per month
• Family allowance: 660 € per month (if eligible, e.g. researcher with dependent spouse and/or children)

The exact gross salary differs depending on the country and host institution. Full details are provided in the detailed descriptions of each position on the project website or during the interview phase.

How to apply

Please click on the application link below to submit your application.