Compiler or Compilation Validation?

摘要

Safety-critical systems increasingly rely on the correct operation of software, and software relies on the correct operation of the compiler. Even for a superficially simple language such as C, the compiler is an extremely complex program, and any development uses only a subset of the compiler's capabilities. This paper builds on the observation that checking the correctness of the output of an algorithm is easier than checking the algorithm itself, and argues that validating a particular compilation is more productive than validating the compiler itself. We describe techniques previously proposed for validating compilations and present a more practical alternative.