The PD-KIND algorithm in the Golem CHC solver

Abstract

PDKind (Property-Directed K-induction) je kombinací IC3 a k-indukce, obou běžně používaných algoritmů pro model checking. PDKind odděluje ověření dosažitelnosti od in- dukčního odůvodňování, což umožňuje nahradit indukci k-indukcí. V této práci se zaměřu- jeme na analýzu a implementaci algoritmu PDKind jako back-endovém enginu v řešiči Golem. Integrací PDKind do Golemu chceme využít jeho jedinečný přístup ke zlepšení efektivity řešiče při řešení různých verifikačních úloh. Implementace bude testována a porovnána s ostatními enginy řešiče Golem na sadě benchmarků, aby se prokázala její srovnatelná efektvita.

PDKind (Property-Directed K-induction) is a combination of IC3 and k-induction, both commonly used model checking algorithms. PDKind separates reachability checking from induction reasoning, allowing induction to be replaced by k-induction. This work focuses on analysing and implementing the PDKind algorithm in the Golem solver as a back-end engine. By integrating PDKind into Golem, our goal is to take advantage of its unique approach to improve the solver's effectiveness in handling various verification tasks. The implementation will be tested and compared to other engines within Golem on a set of benchmarks to demonstrate its comparable efficiency.