The modernisation of the French administration relies on the digitalisation of its services and there are more and more examples of algorithms in charge of applying laws, or event created by laws. In France one might think of:
While CNIL and RGPD are strong tools to enforce control over the storage and use of personal data, not much has been established to enforce control on the correctness and accuracy of the translation of laws to computer code.
These four examples have in common that their source code is open to the public or promised to be. This is in line with recent recommendations of Etalab.
But is opening the source code sufficient to enforce trust from the citizens? In what extent do these algorithms really apply the law, and what were the choices made by their developpers to cope with the ambiguity of lawyers language when it came to actually defining the algorithms? Does the computer code accuratelty implements the algorithms? What tools from Formal Verification can be employed to, at least partially, answer those questions?
A candidate for this internship should:
This interdisciplinary research program has received some support from CNRSand might lead to a funded PhD thesis.
The internship will take place in LaBRI under the co-guidance of Hugo Gimbert, CR CNRS in computer science and Sonia Desmoulins-Canselier, CR CNRS in Law.