Implementing and Evaluating a New Clausification Splitter in Eldarica

Sammanfattning

Formal verification is the process of proving or disproving the correctness of a system using formal specification and mathematical methods. Horn clauses can be used as an intermediate verification language and processed and solved using Horn solvers. An example of a Horn solver is Eldarica. Eldarica receives Horn clauses and applies a set of preprocessing steps to make the clauses easier to solve. One method Eldarica uses for splitting these clauses into other equivalent clauses is a clause splitter, and the purpose of this thesis is to optimize the clause splitter, preventing exponential blow-up from happening when splitting clauses that contain disjunctions. This often occurs when there are a lot of disjunctions in a constraint. To prevent an exponential blow-up, a new implementation of the clause splitter is discussed in this paper to solve the problem. Experimental evaluations have been performed to evaluate the performance of the new implementation, using CHC-COMP benchmarks. The benchmark results highlight differences in clause satisfiability for one benchmark, variations in the number of clauses generated after splitting, and the time required for splitting across different versions.