Verifikace LLVM bit-kódu pomocí systému Hornových klauzulí s omezujícími podmínkami
Thesis title in Czech: | Verifikace LLVM bit-kódu pomocí systému Hornových klauzulí s omezujícími podmínkami |
---|---|
Thesis title in English: | Verification of LLVM bit-code via a system of Constrained Horn Clauses |
Academic year of topic announcement: | 2023/2024 |
Thesis type: | diploma thesis |
Thesis language: | |
Department: | Department of Distributed and Dependable Systems (32-KDSS) |
Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
Author: | hidden - assigned and confirmed by the Study Dept. |
Date of registration: | 02.04.2024 |
Date of assignment: | 15.04.2024 |
Confirmed by Study dept. on: | 20.04.2024 |
Guidelines |
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 IR [3] to the language of CHCs (using appropriate logical theory) and use off-the-shelf CHC solvers to decide if a given safety property can be violated. The implementation will be evaluated using a subset of benchmarks from SV-COMP, a software-verification competition [5]. |
References |
[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 [5] https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main/c |