Evaluation of SMT solvers in abstraction-based software model checking

• Mihály Dobos-Kovács Budapest University of Technology and Economics
• András Vörös Budapest University of Technology and Economics

Resumo

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.

Palavras-chave: model checking, SMT-LIB, formal verification, SMT, CEGAR