# Interpolating Strong Induction

## TL;DR

The paper introduces kAvy, a novel model checking algorithm that combines k-induction with interpolation and Pdr-style generalization, improving efficiency and effectiveness in verifying properties.

## Contribution

kAvy effectively integrates k-induction with interpolation and Pdr techniques, dynamically adjusting induction depth to enhance model checking performance.

## Key findings

- kAvy outperforms Avy and Pdr in efficiency and success rate.
- kAvy is significantly faster on shift benchmarks.
- Using k-induction accelerates verification processes.

## Abstract

The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (Pdr). In this paper, we present kAvy, an SMC algorithm that effectively uses k-induction to guide interpolation and Pdr-style inductive generalization. Unlike pure k-induction, kAvy uses Pdr-style generalization to compute and strengthen an inductive trace. Unlike pure Pdr, kAvy uses relative k-induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and Pdr, and that using k-induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, Pdr and k-induction.