Evaluation of SMT solvers in abstraction-based software model checking
Mihály Dobos-Kovács, András Vörös · 2022
The verification of safety-critical software systems is an algorithmically complex task, which often utilizes SMT (Satisfiability Modulo Theory) solvers for computing abstractions and refinements. It follows that the performance of SMT solvers impacts the performance of the abstraction-refinement-based verification process. Moreover, SMT solvers algorithmically affect the refinement process with either Craig interpolation or unsatisfiable cores. We evaluated eight versions of six different SMT solvers on software verification benchmarks to evaluate their effect on software model checking.