Denis is a PhD student at Inria Paris, part of the Prosecco team. Specialized in programming languages study and design, his main research interest is the crafting of Domain Specific Languages to bring the power of program analysis and proofs to domains such as cryptography, systems engineering, and tax law.
October 20th, 2020 | 43 mins 56 secs
Formal verification has been used to prove the security of cryptographic protocols like Signal and TLS – but can it also be used to verify the correctness of legislation? Denis Merigoux tells us about how Catala wants to use formal methods to verify the French tax code.