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 …
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 …
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.