Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.
Solving Constrained Horn Clauses as C Programs with CHC2C
Lect.Notes Computer
International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024
2024-10-13
18 pages
Article/Chapter (Book)
Electronic Resource
English
Uncertainty-valued horn clauses
TIBKAT | 1994
|A sharp threshold for the phase transition of a restricted Satisfiability problem for Horn clauses
British Library Online Contents | 2001
|SAE Technical Papers | 2006
SAE Technical Papers | 2017