6 papers · 1 filter
Scylla: Translating an Applicative Subset of C to Safe Rust
Aymeric Fromherz, Jonathan Protzenko
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C. Automatically translating C to Rust is thus an appealing course of acti…
Charon: An Analysis Framework for Rust
Son Ho, Guillaume Boisseau, Lucas Franceschino +3
With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosyst…
CUTECat: Concolic Execution for Computational Law
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by com…
Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
Son Ho, Aymeric Fromherz, Jonathan Protzenko
The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foun…
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel se…
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
Raphaël Monat, Aymeric Fromherz, Denis Merigoux
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. Unfortunatel…