Lucas Franceschino

dblp:263/7814 · DBLP profile ↗
← Back
2ranked-venue papers
1as first author
2since 2021 · last 2025
0000-0002-5683-0199ORCID · reported

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 1 first-author · 2 since 2021Theory of computation · 1 · 1 since 2021
YearPublicationVenuePosition
2025 Charon: An Analysis Framework for Rust
abstract
Abstract 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 ecosystem remains relatively young, meaning that every one of these tools has had to re-implement difficult, time-consuming machinery to interface with the Rust compiler and its cargo build system, to hook into the Rust compiler’s internal representation, and to expose an abstract syntax tree (AST) that is suitable for analysis rather than optimized for efficiency. We address this missing building block of the Rust ecosystem, and propose Charon, an analysis framework for Rust. Charon acts as a swiss-army knife for analyzing Rust programs, and deals with all of the tedium above, providing clients with an AST that can serve as the foundation of many analyses. We demonstrate the usefulness of Charon through a series of case studies, ranging from a Rust verification framework (Aeneas), a compiler from Rust to C (Eurydice), and a novel taint-checker for cryptographic code. To drive the point home, we also re-implement a popular existing analysis (Rudra), and show that it can be replicated by leveraging the Charon framework.
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
CAV (4)3
2021 Verified Functional Programming of an Abstract Interpreter
Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
SAS1