Les systèmes experts juridiques s'appuient régulièrement sur des calculs de date pour déterminer l'éligibilité des citoyennes et citoyens aux prestations sociales ou si une demande a été déposée dans les délais. Des membres du Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) ont reçu un prix à ETAPS 2024 pour le meilleur outil.
Malheureusement, l'arithmétique des dates présente de nombreux cas particuliers, qui sont traités différemment d'une bibliothèque à l'autre, ce qui rend la transcription fidèle de la loi dans le code sujette à des erreurs et peut entraîner de lourdes conséquences financières et juridiques pour les utilisateurs. Dans le travail publié à la conférence internationale ESOP, nous visons à fournir une base solide pour l'arithmétique des dates travaillant sur les jours, les mois et les années. Nous présentons d'abord une nouvelle sémantique formelle pour les calculs de dates, et établissons formellement plusieurs propriétés sémantiques par le biais d'une mécanisation dans l'assistant de preuve F⋆. En nous appuyant sur cette sémantique, nous proposons ensuite une analyse statique par interprétation abstraite pour détecter automatiquement les ambiguïtés dans les calculs de dates. Nous intégrons enfin notre approche dans le langage Catala, un langage à domaine spécifique pour formaliser certaines lois calculatoires telles que les impôts et les prestations sociales. Nous utilisons notre approche pour analyser l'implémentation Catala des allocations logement, ce qui conduit à la découverte de plusieurs ambiguïtés liées aux calculs sur les dates. Ces travaux font partie de l'action exploratoire Inria, portée conjointement par Raphaël Monat (équipe Sycomores, Lille) et Aymeric Fromherz (équipe Prosecco, Paris).