@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 {392,
	title = {Reachability Analysis for Multiloop Programs Using Transition Power Abstraction},
	booktitle = {FM 24},
	year = {2024},
	month = {09/2024},
	abstract = {A wide variety of algorithms is employed for the reachability analysis of programs with loops but most of them are restricted to single loop programs. Recently a new technique called Transition Power Abstraction (TPA) showed promising results for safety checks of software. In contrast to many other techniques TPA efficiently handles loops with a large number of iterations.
This paper introduces an algorithm that enables the effective use of TPA for analysis of multiloop programs. The TPA-enabled loop analysis reduces the dependency on the number of possible iterations. Our approach analyses loops in a modular manner and both computes and uses transition invariants incrementally, making program analysis efficient. The new algorithm is implemented in the Golem solver. Conducted experiments demonstrate that this approach outperforms the previous implementation of TPA and other competing tools on a wide range of multiloop benchmarks.},
	author = {Konstantin Britikov and Martin Blicha and Natasha Sharygina and Grigory Fedyukovich}
}
@conference {390,
	title = {SolTG: A CHC-based Solidity Test Case Generator},
	booktitle = {Computer Aided Verification},
	year = {2024},
	abstract = {<p>Test coverage is an important metric for the development of blockchain smart contracts. In this paper, we present SolTG, an automated CHC-based test case generator for Solidity smart contracts. SolTG exhaustively enumerates symbolic formulas and makes calls to SMT solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters, which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of generating high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG and the translation of smart contracts into their CHC representation that the tool relies on. We also present the experimental results for test generation on the regression and industrial benchmarks.</p>
},
	url = {https://link.springer.com/content/pdf/10.1007/978-3-031-65627-9_23.pdf},
	author = {Konstantin Britikov and Ilia Zlatkin and Grigory Fedyukovich and Leonardo Alt 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}
}
