PHD scholarship (M/F): Formal Verification Techniques for Reversible Languages
New
- FTC PhD student / Offer for thesis
- 36 mounth
- Doctorate
This offer is available in English version
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
Laboratoire d'Informatique, Signaux et Systèmes de Sophia Antipolis
Contract Type
FTC PhD student / Offer for thesis
Working hHours
Full Time
Workplace
06903 VALBONNE
Contract Duration
36 mounth
Date of Hire
01/09/2026
Remuneration
2300 € gross monthly
Apply Application Deadline : 19 June 2026 23:59
Job Description
Thesis Subject
In RC verifying forward computations equipped with distributed backtracking on non-observable actions is equivalent to verifying their causal compression which may be significantly smaller in size and therefore much more efficiently verifiable. Also, classical Linear Temporal Logic (LTL) and unfolding algorithms can be used to model check reversible systems, as an LTL formula with a past operator can be translated in terms of "future" states. This may not be the case with logics such as Computation Tree Logic (CTL) and logics for truly concurrent systems. We plan to 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. Specifically, for concurrent reversible processes, we will investigate the development of appropriate session type disciplines.
Your Work Environment
Laboratoire I3S, Team Comred
Compensation and benefits
Compensation
2300 € gross monthly
Annual leave and RTT
44 jours
Remote Working practice and compensation
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
About the offer
| Offer reference | UMR7271-CINDIG-002 |
|---|---|
| CN Section(s) / Research Area | Information sciences: bases of information technology, calculations, algorithms, representations, uses |
About the CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.