@article {399,
	title = {Golem: a flexible and efficient solver for constrained Horn clauses},
	journal = {Formal Methods in System Design},
	year = {2025},
	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.},
	doi = {https://doi.org/10.1007/s10703-025-00470-9},
	url = {https://rdcu.be/efgv8},
	author = {Martin Blicha and Konstantin Britikov and Natasha Sharygina}
}
@conference {382,
	title = {The Golem Horn Solver},
	booktitle = {Computer Aided Verification},
	year = {2023},
	abstract = {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.},
	doi = {https://doi.org/10.1007/978-3-031-37703-7\_10},
	url = {https://verify.inf.usi.ch/sites/default/files/cav23-final109.pdf},
	author = {Martin Blicha and Konstantin Britikov and Natasha Sharygina}
}
