AEx AVoCAT
Title: Automated Verification of CATala programs
Inria Exploratory Action 2023
Coordinators: Raphaël Monat, co-PI with Aymeric Fromherz (Prosecco, Inria Paris)
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. These tools are intended for use by lawyers and IT specialists in administrations, who translate the law into computer code in order to apply it automatically on massive scales or for economic modeling purposes.
SYWEXT
Title: Symbolic Worst-Case Execution Time evaluation with global contexts
ANR JCJC project, AAP 2019
Coordinator: Clément Ballabriga
Hard real-time safety critical systems are systems whose correctness depends not only upon the correctness of the produced results, but also on the time at which they are produced. A missed deadline may compromise the functionality of the system, and in some extreme cases, even cause loss of human lives. Enforcing such deadlines requires computing the Worst-Case Execution Time (WCET). In critical systems, in order to guarantee safety, the WCET is usually computed by static analysis. While WCET is usually computed as a constant value, it is beneficial to compute a symbolic WCET, because it enables modular WCET analysis, component reuse, library or system call integration, or analysis of adaptive real-time systems. The most common WCET analysis technique is the Implicit Path Enumeration Technique (IPET). IPET-based analyses are unfortunately hard to perform parametrically due to a very high resolution complexity. Tree-based WCET analysis is an alternative to IPET approaches, that usually have shorter analysis time, but suffer from inability to represent some complex timing effects. In order to compute a precise symbolic WCET analysis, our long-term objective is to design a tree-based parametric approach that is sufficiently powerful to express a wide range of hardware and software facts, while retaining a tractable analysis complexity.
