Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled …

AEx AVoCAT: Automated Verification of Catala programs

Catala is a new programming language, designed to be understood by legal experts and to follow the structure of legislative texts, transforming law into code. We propose to explore the automatic verification of Catala programs, in order to obtain tools that for that tax and social security laws satisfy safety and correctness properties, generating concrete counter-examples where appropriate.