For full conference details, please visit the 2018 European LLVM Developers’ Meeting website.
Back To Schedule
Monday, April 16 • 11:15am - 11:35am
Using LLVM in a Model Checking Workflow

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

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).


Gyula Sallai

Budapest University of Technology and Economics

Monday April 16, 2018 11:15am - 11:35am BST
Bristol 1 & 2