The Golem Horn Solver

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 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.

BibTeX:

@inproceedings{blicha_golem_2023,
    title = {{The Golem Horn Solver}},
    author = {Blicha, Martin and Britikov, Konstantin and Sharygina, Natasha},
    year = {2023},
    booktitle = {{Computer Aided Verification}},
    editor = {Enea, Constantin and Lal, Akash},
    publisher = {Springer Nature Switzerland},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-031-37703-7_10},
    isbn = {978-3-031-37703-7},
    pages = {209--223},
}

Proceedings paper