Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution)

Title:

Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution)

Authors:

M. Blicha, J. Kofroň, O. Glitta

Publication:

Tools and Algorithms for the Construction and Analysis of Systems

DOI:

Year:

2026

ISBN:

978-3-032-22749-2

Abstract:

Hornix is a software verification tool for C programs based on a translation first to LLVM intermediate representation (IR) and subsequently to constrained Horn clauses (CHCs). It extends LLVM with a transformation pass that constructs a system of CHCs from the LLVM IR representation and the safety property of the program. The resulting CHC system is then passed to a backend Horn solver, such as Eldarica, Golem, or Z3-Spacer. Hornix is currently in an early stage of development and supports reasoning about safety properties of integer programs only.

BibTeX:

@inproceedings{blicha_hornix_2026,
    title = {{Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution)}},
    author = {Blicha, Martin and Kofroň, Jan and Glitta, Oliver},
    year = {2026},
    booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems}},
    editor = {Junges, Sebastian and Katz, Guy},
    publisher = {Springer Nature Switzerland},
    location = {Cham},
    doi = {10.1007/978-3-032-22749-2_28},
    isbn = {978-3-032-22749-2},
    pages = {530--535},
    shorttitle = {Hornix},
}