Golem: a flexible and efficient solver for constrained Horn clauses

TitleGolem: a flexible and efficient solver for constrained Horn clauses
Publication TypeJournal Article
Year of Publication2025
AuthorsBlicha, Martin, Britikov Konstantin, and Sharygina Natasha
JournalFormal Methods in System Design
Abstract

The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this work we present Golem, a flexible and efficient solver for satisfiability of CHCs over linear real and integer arithmetic. Golem provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of Golem and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.

URLhttps://rdcu.be/efgv8
DOI10.1007/s10703-025-00470-9