Formal Verification of Safety Properties Using Interpolation and k-induction

TL;DR

This paper implements and compares two symbolic model checking algorithms, interpolation-based and k-induction, using SAT/SMT solvers to verify safety properties in systems.

Contribution

It introduces implementations of two symbolic model checking algorithms and provides a comparative analysis of their effectiveness.

Findings

Both algorithms successfully verify safety properties.

Interpolation-based model checking shows different strengths compared to k-induction.

The comparative analysis highlights scenarios where each method performs best.

Abstract

This technical report presents implementation of two symbolic model checking algorithms that use SAT/SMT Solvers, namely interpolation based model checking and k-induction based model checking. We also do a comparative analysis of these two model checking algorithms.