3 papers
cs.PL2026
DueList: A Theory of Lists with Combinators for SMT Solvers
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or s…
cs.PL2024
Easing Maintenance of Academic Static Analyzers
Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some need to be maintained in order to enable buildi…
cs.PL2020
A Modern Compiler for the French Tax Code
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
In France, income tax is computed from taxpayers' individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP)…