PhD Position F/M Formal Verification of Liveness in Distributed Systems using Reinforcement Learning

PhD Position F/M Formal Verification of Liveness in Distributed Systems using Reinforcement Learning Download job offer in PDF format Contract type : Fixed-term contract Level of qualifications required : Graduate degree or equivalent Fonction : PhD Position About the research centre or Inria department The Inria center at the University of Rennes is one of eight Inria centers and has more than thirty research teams. The Inria center is a major and recognized player in the field of digital sciences. It is at the heart of a rich ecosystem of R&D and innovation, including highly innovative SMEs, large industrial groups, competitiveness clusters, research and higher education institutions, centers of excellence, and technological research institutes. Context This is a joint PhD between Inria Rennes and Mitsubishi Electric R&D Centre Europe (MERCE) located in Rennes, France, supervised by Ocan Sankur (Irisa - Inria), Florian Faissole, and Nicolas Waldburger (MERCE). Candidates may contact supervisors for more information: ocan.sankur@cnrs.fr, f.faissole@fr.merce.mee.com, n.waldburger@fr.merce.mee.com Applications must be submitted on the following website: https://www.mitsubishielectric-rce.eu/job/phd-thesis-proposal-3-years-m-reinforcement-learning-for-formal-verification-of-liveness-in-distributed-systems/ Assignment A livelock in a concurrent software is a situation where two threads are continuously executed, but each thread requires a resource owned by the other thread, and they enter a loop where no progress is made by any of the threads. One example is two polite persons trying to eat soup with a shared spoon: they both request to eat soup, but the person holding the spoon is too polite and passes it to the other person before eating the soup. The other person has the same behavior, so they end up passing the spoon to each other and no one ever actually eats the soup. Livelocks are notoriously difficult to detect because it is difficult to distinguish them from a trace where the threads just need to wait for a long time before making progress (say, because they are waiting for some computations to terminate). Theoretically, the difficulty can be explained by the fact that absence of livelocks is a liveness property (a proof of violation is necessarily an infinite execution), and not a safety property (for which a proof of violation could be finite). Directed testing and fuzzing have been used to test concurrent and distributed systems. Some of these techniques use reinforcement learning, where the tester is seen as a policy, and the goal is to find the best tester which achieves maximal coverage, or some other criterion such as reaching a specific location in the code. This has been used in symbolic/concolic execution [5, 4], and fuzzing [1]. Reinforcement learning or other machine learning techniques based on neural networks have been used to prove the termination of programs but also to establish their satisfaction of temporal properties [3]. Objectives We are interested in developing algorithms for automatically proving the absence of livelocks or detecting livelocks bugs in distributed protocols using directed testing algorithms. We suggest developing deep RL algorithms to analyze maximal wait times in distributed protocols. The wait time is the number of steps a process is executed before it gains access to a resource. There are no livelocks if the wait times are always finite. The work consists in modeling this problem as an RL problem, choosing the right rewards and RL algorithms, and making sure it scales to real implementations of distributed algorithms. Here the RL agent chooses at each step the schedule, that is, which process to execute, whether there are packet losses etc. and observes the next global state of the system. It receives a reward of 1 at each step a process waiting to access a resource is executed but without accessing that resource. Thus, the distributed protocol can be seen as a game which the RL agent must learn how to play to exhibit the worst-case behavior. The model and RL algorithms can be chosen either to attempt to prove the absence of livelocks and compute bounds on wait times, or to detect livelock bugs. The precise direction to be taken and the weight given to RL versus formal verification in this work can be chosen according to the student’s background and preferences.The work also includes an extensive bibliographic study, the development of the above algorithms, implementation and experiments. References [1] Konstantin Bottinger, Patrice Godefroid, and Rishabh Singh. Deep reinforcement fuzzing. In 2018 IEEE Security and Privacy Workshops (SPW), pages 116–122. IEEE, 2018. [2] Malay K. Ganai. Dynamic livelock analysis of multi-threaded programs. In Shaz Qadeer and Serdar Tasiran, editors, Runtime Verification, pages 3–18, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [3] Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. Neural model checking. arXiv preprint arXiv:2410.23790, 2024. [4] Jinkyu Koo, Charitha Saumya, Milind Kulkarni, and Saurabh Bagchi. Pyse: Automatic worstcase test generation by reinforcement learning. In 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST), pages 136–147, 2019. [5] Ciprian Paduraru, Miruna Paduraru, and Alin Stefanescu. Optimizing decision making in concolic execution using reinforcement learning. In 2020 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pages 52–61, 2020. [6] Richard S Sutton, Andrew G Barto, et al. Reinforcement learning: An introduction. MIT press Cambridge, 1998.Thanks for providing us an application letter and your CV mentioning the reference HMTFT043 [7] Andrea Borgarelli, Constantin Enea, Rupak Majumdar, and Srinidhi Nagendra. 2024. Reward Augmentation in Reinforcement Learning for Testing Distributed Systems. Proc. ACM Program. Lang. 8, OOPSLA2, Article 339 (October 2024), 27 pages. https://doi.org/10.1145/3689779 Main activities Conduct research within this PhD. Skills The candidate must have a strong mathematical background in logic, automata, and formal verification. Alternatively, a strong background theoretical background in reinforcement learning is also welcome. A previous research experience (such as research internship) is a must. A research master's degree (ongoing or obtained) is required in one of these fields with strong theoretical foundations. Please justify your theoretical background (lists of courses taken, grades, internship reports, publications), and provide references of persons who can recommend you (such as former internship or master's supervisors). Benefits package • Subsidized meals • Partial reimbursement of public transport costs • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.) • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours • Professional equipment available (videoconferencing, loan of computer equipment, etc.) • Social, cultural and sports events and activities Remuneration monthly gross salary 2300 euros Apply for this position Share • Facebook • Linkedin • Twitter • Email General Information • Theme/Domain : Proofs and Verification Software engineering (BAP E) • Town/city : Rennes • Inria Center : Centre Inria de l'Université de Rennes • Starting date : 2026-10-01 • Duration of contract : 3 years • Deadline to apply : 2026-08-31 Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed. Instruction to apply Please submit online : your resume, cover letter and letters of recommendation eventually Defence Security : This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment. Recruitment Policy : As part of its diversity policy, all Inria positions are accessible to people with disabilities. Contacts • Inria Team : DEVINE • PhD Supervisor : Sankur Ocan / ocan.sankur@irisa.fr About Inria Inria, the French national institute for research in digital science and technology, supports the French government in national research and innovation strategies in the digital field, acting as Digital Programs Agency. Inria leads over 300 research and innovation projects with its 3,500 scientists, engineers, and support staff, in partnership with universities and the digital ecosystem (businesses, entrepreneurs, and public stakeholders). Together, we explore strategic fields such as artificial intelligence, cybersecurity, quantum computing, cloud technologies, digital transformation in healthcare, digital twins, and digital technologies for defence. We develop practical solutions such as software, tech startups, partnerships with national companies, and cutting-edge training programmes. Our goal is to drive scientific, technological, and industrial excellence to ensure France’s digital sovereignty.