The Golem Horn Solver

TitleThe Golem Horn Solver
Publication TypeConference Paper
Year of Publication2023
AuthorsBlicha, Martin, Britikov Konstantin, and Sharygina Natasha
Conference NameComputer Aided Verification

The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verifi- cation 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 CHC 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.