Verification of LLVM bit-code via a system of constrained Horn clauses

Target

Master thesis or Research project

Contact

• Jan Kofroň
• Martin Blicha

An approach to verification of software is model checking, which creates a logical model of the program and then checks the model for a given safety property. A logical formalism of constrained Horn clauses (CHCs) [1,2] represents a very useful model of programs that enriches the simple logical representation of theories of first-order logic with semantics being able to capture the behaviour of loops and recursion.

The goal of this thesis is to design and implement a translation from (a subset of) LLVM bit-code [3] to the language of CHCs (using appropriate logical theory) and experiment with different modelling approaches and different CHC back-ends.

1. Horn clauses: https://en.wikipedia.org/wiki/Horn_clause
2. https://arieg.bitbucket.io/pdf/satsmtar-school-2018.pdf
3. LLVM project: https://llvm.org/
4. Bjørner N., Gurfinkel A., McMillan K., Rybalchenko A. (2015) Horn Clause Solvers for Program Verification. In: Beklemishev L., Blass A., Dershowitz N., Finkbeiner B., Schulte W. (eds) Fields of Logic and Computation II. Lecture Notes in Computer Science, vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_2