|
Compilers are crucial components of the computing ecosystem transforming rich abstractions in many source languages into multiple target architectures. Compiler bugs break all the verification guarantees at the source code level and can lead to disasters in safety-critical domains. Although testing can reduce such errors, testing is infeasible for all inputs with richer abstractions and targets. In contrast to testing, formal verification can provide robust assurances.
The goal of this project is to design pragmatic formal techniques that can be incorporated into a mainstream compiler for regular use by developers. The LLVM compiler is chosen as the object of study, which is widely used at Apple, Google, Nvidia, and by open-source software.
|
Sign in
to view more information about this project.
