Phd Position F/m Formal Verification of Higher-order, Probabilistic Programs

_Le descriptif de l’offre ci-dessous est en Anglais_

**Type de contrat**: CDD

**Niveau de diplôme exigé**: Bac + 5 ou équivalent

**Fonction**: Doctorant

**A propos du centre ou de la direction fonctionnelle**:
The Inria center at Université Côte d'Azur includes 42 research teams and 9 support services. The center’s staff (about 500 people) is made up of scientists of different nationalities, engineers, technicians and administrative staff. The teams are mainly located on the university campuses of Sophia Antipolis and Nice as well as Montpellier, in close collaboration with research and higher education laboratories and establishments (Université Côte d'Azur, CNRS, INRAE, INSERM...), but also with the regional economic players.

With a presence in the fields of computational neuroscience and biology, data science and modeling, software engineering and certification, as well as collaborative robotics, the Inria Centre at Université Côte d'Azur is a major player in terms of scientific excellence through its results and collaborations at both European and international levels.

**Contexte et atouts du poste**:
This PhD thesis project is part of the ANR project HOPR (Higher-Order Probabilistic and resource-aware Reasoning) (ANR-24-CE48-5521-01) coordinated by P. Baillot, starting in 2025 and aiming at defining expressive logical frameworks, dealing in particular with higher-order computation and probabilities, which can serve to reason on cryptographic primitives and protocols and on differential privacy. The project has three partner sites: INRIA Lille/CRIStAL; INRIA Paris; IRISA Rennes and INRIA Sophia-Antipolis. It is starting in January 2025 for 4 years.

The recruited PhD student will carry out her/his research within the SPLITS and OLAS project-teams at INRIA Sophia Antipolis, under the supervision of B. Gregoire and M. Avanzini

**Mission confiée**:
Randomized computation has emerged as a highly effective extension of the standard deterministic computational model, especially in recent decades. Randomization plays a key role among many areas of computer science, e.g., zin computational complexity, artificial intelligence, security and privacy.

Dijkstra’s weakest-precondition predicate transformers are certainly among the most effective tools in the field of program semantics and verification. Over the past decade, such constructions have been generalized to probabilistic programs: in this context, it is natural that the truth of a formula becomes quantitative in nature, e.g., truth values turn into probabilities. While this methodology is well-established for probabilistic imperative programs [Kozen, 1981; McIver and Morgan, 2005; Avanzini et al. 2023,2024], its extension to
higher-order programs remains underexplored. This is unfortunate, as e.g. game-based cryptographic proofs inherently center around the analysis of higher-order, probabilistic programs.

2012], a proof assistant designed for game-based cryptographic proofs, which has been extensively used in recent years to verify cryptographic routines, including post-quantum schemes such as Kyber [Almeida et al., 2024].

References:
[Almeida et al. 2024] José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub: Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) 2024: 384-421

[Avanzini et al., 2024] Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni: Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8(OOPSLA1): 784-809 (2024)

[Avanzini et al., 2023] Martin Avanzini, Georg Moser, Michael Schaper: Automated Expected Value Analysis of Recursive Programs. Proc. ACM Program. Lang. 7(PLDI): 1050-1072 (2023)

[Avanzini et al., 2021] Martin Avanzini, Gilles Barthe, Ugo Dal Lago: On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021)

[Barthe et al., 2012] Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin: Computer-Aided Cryptographic Proofs. ITP 2012: 11-27

[Kozen 1981] Dexter. Kozen. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22, 3 (1981), 328-350. (1981)

[McIver and Morgan, 2005 ] Annabelle McIver and Carroll Morgan. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media. (2005)

**Principales activités**:

- Carry out the PhD research project on Verification of Higher-Order, Probabilistic Programs.
- Collaborate with other team members and with the ANR HOPR project partners
- Disseminate research results, by publications and presentations at international conferences

**Compétences**:
Some basic knowledge of either type systems, proof