Generating Non-Linear Interpolants by Semidefinite Programming

TL;DR

This paper introduces a novel method for generating non-linear interpolants using semidefinite programming, enhancing verification techniques for hardware and software by enabling polynomial interpolant synthesis.

Contribution

It presents the first approach for constructing polynomial interpolants via semidefinite programming, expanding the scope of interpolation methods in verification.

Findings

Successfully applied to program verification examples

Demonstrated effectiveness in synthesizing polynomial interpolants

Provides a new tool for non-linear interpolation in formal methods

Abstract

Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model check- ing, CEGAR, SMT, etc., whose hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In this paper, we provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples.