Podpora práce s pamětí (heap) v nástroji Hornix
| Název práce v češtině: | Podpora práce s pamětí (heap) v nástroji Hornix |
|---|---|
| Název v anglickém jazyce: | Heap Support For Hornix |
| Akademický rok vypsání: | 2025/2026 |
| Typ práce: | diplomová práce |
| Jazyk práce: | |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: |
| Zásady pro vypracování |
| 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 extend the implementation of Hornix [5] – a LLVM [3] plugin – by support for instructions for dynamic heap de/allocation. This means supporting a larger set of LLVM IR bitcode instructions, in turn supporting a larger set of input C/C++ programs. Analysis of the required set of LLVM IR instructions that should be implemented should stem from analysis of a suitable set of input C/C++ programs. |
| Seznam odborné literatury |
| [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] Hornix: https://github.com/d3sformal/hornix |