Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Martin Blicha,
  • Jan Kofroň,
  • Oliver Glitta

摘要

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.