Selected activities
LLVMC++Frama-CFlex/BisonXcode
I developed a framework built on top of the LLVM compiler that leverages annotations produced by Crowd Source Formal Verification (a DARPA-funded project that used video games to solve complex underlying problems). These annotations are integrated during the compilation process to enhance LLVM optimizations and reduce the overhead of enforcing run-time memory safety.