Arthur Gontier

Postdoctoral researcher

Subject: Constraint solver producing proof of reasoning

FATA team, University of Glasgow

About me

Hi there! I am Arthur Gontier. Since January 2024, I am a researcher in the FATA team in the University of Glasgow. I am working with Ciaran McCreesh, Matthew McIlree and the VeriPB group on constraint solvers that produces proofs of reasoning.

Before that, I was a PhD student in symmetric cryptanalysis with declarative languages in the CAPSULE team in Rennes supervised by Stéphanie Delaune, Patrick Derbez and Charles Prud'homme. My PhD thesis can be found here. I was working on symmetric cryptanalysis problems like Cube attacks or Differential attacks. To do so, I used several solvers or even dedicated algorithms.

In these three years, we published three papers in cryptography related conferences where we used many optimisation methods, (CP MILP SAT and dedicated algorithms). To tackle the hard problems of cryptography with CP, we often needed to make new constraints. Indeed, there are very specific cryptographic properties we modeled in graph constraints or set constraints for solvers like Choco and Chuffed.

I also worked on explanations and conflict analysis. In a CP 2020 workshop, we proposed an explanation generator to help the use of explanations in CP solvers.

Finally, I participated to TAGADA, a generic tool to perform differential cryptanalysis on generic block ciphers with constraint programming. The idea is the following: anyone can model any cipher and the tool will perform differential cryptanalysis on it.

Before that, I had a Master's Degree in Nantes and Bruxelles focusing on optimisation techniques with CP teachers like Nicolas Beldiceanu and Eric Monfroy. I also did several research internships, on multi objective optimisation, static program analysis and CP explanations. Feel free to check my CV for more details.

See my work

Publications

  • VeriPB proof trimming. 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. Under submission, 2026.
  • 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, et al. Proceedings of the 40th AAAI Conference on Artificial Intelligence (AAAI 2026), 2026. [pdf] [Code]
  • A CP-based automatic tool for instantiating truncated differential characteristics. François Delobel, Patrick Derbez, Arthur Gontier, Loïc Rouquette, and Christine Solnon. International Conference on Cryptology in India (INDOCRYPT 2023), pages 247–268. Springer, 2023. [pdf] [Slides] [Code]
  • New algorithm for exhausting optimal permutations for generalized feistel networks. Stéphanie Delaune, Patrick Derbez, Arthur Gontier, and Charles Prud’homme. In Takanori Isobe and Santanu Sarkar, editors, Progress in Cryptology - INDOCRYPT 2022 - 23rd International Conference on Cryptology in India, Kolkata, India, December 11-14, 2022, Proceedings, volume 13774 of Lecture Notes in Computer Science, pages 103–124. Springer, 2022. [pdf] [Slides] [Talk] [Code]
  • A simpler model for recovering superpoly on trivium. Stéphanie Delaune, Patrick Derbez, Arthur Gontier, and Charles Prud’homme. In Riham AlTawy and Andreas Hülsing, editors, Selected Areas in Cryptography - 28th International Conference, SAC 2021, Virtual Event, September 29 - October 1, 2021, Revised Selected Papers, volume 13203 of Lecture Notes in Computer Science, pages 266–285. Springer, 2021 [pdf] [Slides] [Talk] [Code]
  • Diffusion totale dans le schéma de Feistel généralisé. Stéphanie Delaune, Patrick Derbez, Arthur Gontier, and Charles Prud’Homme. In ROADEF 2022 : 23ème congrès annuel de la Société Française de Recherche Opérationnelle et d’Aide à la Décision, Villeurbanne - Lyon, France, February 2022. INSA Lyon [pdf] [Slides]
  • Conflict analysis in CP solving: Explanation generation from constraint decomposition. Arthur Gontier, Charlotte Truchet, and Charles Prud’Homme. In CP 2020: 26th International Conference on Principles and Practice of Constraint Programming: Workshop: From Constraint Programming to Trustworthy AI, volume 12333 of Lecture Notes in Computer Science book series (LNCS) Also part of the Programming and Software Engineering book sub series (LNPSE), Louvain-la-Neuve, Belgium, September 2020. [pdf] [Slides] [Code]

Invited Talks

  • Progress on VeriPB proof trimming. Arthur Gontier. International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2025. [Slides] [Talk]
  • First results on VeriPB proof trimming. Arthur Gontier. International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2024. [Slides] [Talk]

PhD

  • [en] Cryptanalysis of symmetric cipher using generic solvers [fr] 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 live]

Teaching

  • Graph theory, 2020, Université de Rennes 1, Bachelor 3, 24H
  • Mixed Integer Linear programming, 2020, Université de Rennes 1, Master 1, 12H
  • Functional Programming, 2021, INSA Rennes, Master 1, 18H
  • Computer science, 2021-2023, Université de Rennes 1, Bachelor 1, 72H
Contact me

Contact me

arthur.pro.gontier@gmail.com

arthur.gontier@glasgow.ac.uk

Find me

Office G091, School of Computing Science, Sir Alwyn Williams Building, Glasgow

Home