# Golem: a flexible and efficient solver for constrained Horn clauses

## TL;DR

Golem is a new tool that efficiently solves logical problems used in program verification.

## Contribution

Golem introduces a flexible and efficient CHC solver with a novel model-checking algorithm called TPA.

## Key findings

- Golem integrates tightly with SMT solvers for improved efficiency.
- The TPA algorithm enables deep exploration in solving CHCs.
- Extensive evaluation shows Golem is competitive with existing solvers.

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