Automatically Deriving Checkers for Compiler Verification

Abstract

Compiler verification is a hard problem. Verification costs can be reduced by means of translation validation, where individual runs of the compiler are verified, rather than all possible runs. This approach is used for the certification of the Plutus TX compiler. But this currently requires a handwritten decision procedure for each pass of the compiler. This thesis investigates the possibility of automatically deriving these decision procedures. This would reduce the complexity of verification of the compiler, because its derived checkers are less laborious to acquire, easier to maintain, and less prone to human errors.