Luce: A formal methodology and algorithms for compile-time reasoning of memory corruption- related emergent behaviors (2020-)
The Luce project is an investigation into how to automatically reason about memory corruption-related weird machines.
To achieve this goal, we are exploring algorithmic techniques that, at compile-time, compute a class of memory corruption-related, unintended emergent behaviors that are formally proven accurate.
While the term Luce is an acronym, standing for LLVM with formal memory usage certificates, it is also Latin and Italian for light and is pronounced as such.
Supported by: DARPA
Participating CS members: Freek Verbeek, Nico Naus, Timmy Weerwag.