Formal verification can be used to show the presence or absence of specific type of errors in a computer program. Formal verification is usually done by transforming the already implemented source code into a formal model, then mathematically proving certain properties of that model (e.g. an erroneous state in the model cannot be reached). The theta verification framework provides a well-defined formal model suitable for checking imperative programs. In this talk, we present an LLVM IR frontend for theta, which bridges the gap between formal verification frameworks and the LLVM IR representation. Leveraging the LLVM IR as the frontend language of the verification workflow simplifies the transformation and allows us to easily add new supported languages.
However, these transformations often yield impractically large models, which cannot be checked within a reasonable time. Therefore size reduction techniques need to be used on the program, which can be done by utilizing LLVM's optimization infrastructure (optimizing for size and simplicity rather than execution time) and extending it with other reduction algorithms (such as program slicing).
