Because compilers are complex and play a critical role in the software ecosystem, formally verification their correctness is a problem of great importance. However, the compiler verification problem is also notoriously hard. In my bachelor's thesis, I developed a novel verification approach which makes the verification problem significantly easier within the important domain of logic programming languages.
My approach, which I call the Certifying Abstract Machine approach, is an instance of certifying compilation, which is a form of verification where every run of the compiler produces a formal proof that the given compiler output is a correct compilation of the given input. In the Certifying Abstract Machine approach, a compiler targets a dependently-typed virtual machine whose type system is strong enough to formally prove that the compiled program meets its correctness specification. In this way, the typechecker for the virtual machine serves as a domain-specific proof checker for the compiler correctness proofs.
When applied to logic programming, this approach is aided by the fact that logic programs are their own specifications. A Prolog program (ignoring order of execution) is simply a signature of inference rules, which can just as easily be expressed in a formal logical framework such as LF. (Partial) correctness of a compiled Prolog program means that it only produces proofs that follow from the signature specified in the Prolog program, or equivalently, an LF signature. By embedding LF in the type system of the virtual machine, we provide a way to show that all well-typed programs obey their LF signatures.
Brandon Bohrer and Karl Crary.
TWAM: A Certifying Abstract Machine for Logic Programs.
Certifying Compilation for Logic Programs.
CMU SCS Honors Thesis, 2014.
Available upon request. The arXiv paper is recommended instead.