Arthur Gontier

About

Since January 2024 I am a postdoctoral researcher at the University of Glasgow, in the FATA section. I work with Ciaran McCreesh, Matthew McIlree and the VeriPB group on proof producing constraint solvers.

Before that I was a PhD student in symmetric cryptanalysis with declarative languages. I used several kinds of solvers, constraint programming, linear programming and Boolean satisfiability, as well as dedicated algorithms, to find differential characteristics or mount cube attacks, for example. I was working in the CAPSULE team in Rennes, supervised by Stéphanie Delaune, Patrick Derbez and Charles Prud'homme.

Earlier, I obtained a Master's degree in Optimisation and Operational Research in Nantes and Brussels and I did several research internships on multi-objective optimisation, static program analysis and CP explanations.

Research interests

• Proof logging for constraint solvers. Making solvers justify every inference they make, so that their answers can be checked independently. My current work is on trimming VeriPB proofs to make verification tractable, and to explain the critical reasoning of solvers.
• Generic solvers for cryptanalysis. Modelling cryptographic properties so that solvers can reason about them can lead to new discoveries, and if those solvers are certifying, we can derive security guarantees from their proofs.
• Conflict analysis, explanations and proof logging. To make explanations and proof logging easier to use in CP solvers, I am interested in generating explanations for global constraints from their decompositions, and in externalising the justifications of propagators.
• Generic cryptanalysis tooling. I contributed to TAGADA, a tool where anyone can model a block cipher and have differential cryptanalysis performed on it automatically. Such tools are valuable to automate and speed up cryptanalysis.

Publications

International peer-reviewed conferences

1. Trimming pseudo-Boolean proofs Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola‑Pardo, Mark Turnbull Formal Methods in Computer-Aided Design (FMCAD 2026), Graz, Austria, 14–18 September 2026 — accepted for publication pdf code
2. Faster certified symmetry breaking using orders with auxiliary variables Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola‑Pardo, Yong Kiam Tan. 40th AAAI Conference on Artificial Intelligence (AAAI 2026), 2026 pdf code
3. A CP-based automatic tool for instantiating truncated differential characteristics François Delobel, Patrick Derbez, Arthur Gontier, Loïc Rouquette, Christine Solnon International Conference on Cryptology in India (INDOCRYPT 2023), pages 247–268, Springer, 2023 pdf slides code
4. New algorithm for exhausting optimal permutations for generalized Feistel networks Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme Progress in Cryptology – INDOCRYPT 2022, LNCS 13774, pages 103–124, Springer, 2022 pdf slides talk code
5. A simpler model for recovering superpoly on Trivium Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme Selected Areas in Cryptography – SAC 2021, LNCS 13203, pages 266–285, Springer, 2021 pdf slides talk code

Workshops and national conferences

1. Diffusion totale dans le schéma de Feistel généralisé Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme ROADEF 2022, 23^e congrès annuel de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, Villeurbanne – Lyon, France, February 2022 pdf slides
2. Conflict analysis in CP solving: explanation generation from constraint decomposition Arthur Gontier, Charlotte Truchet, Charles Prud'homme CP 2020 workshop “From Constraint Programming to Trustworthy AI”, 26th International Conference on Principles and Practice of Constraint Programming, Louvain-la-Neuve, Belgium, September 2020 pdf slides code

Invited talks

1. Trimming pseudo-Boolean proofs International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2026 slides
2. Progress on VeriPB proof trimming International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2025 slides talk
3. First results on VeriPB proof trimming International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2024 slides talk

PhD thesis

1. Cryptanalysis of symmetric ciphers using generic solvers — Utilisation de solveurs génériques pour la cryptanalyse de chiffrements symétriques Arthur Gontier Thèse de doctorat, Université de Rennes, 2023 pdf slides defence

Teaching

Contact