Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic

EasyChair Preprint no. 10000

Abstract

Interpolants are central for symbolic model-checking and synthesis of invariants in program verification. Over the past couple of decades several methods have been developed for extracting interpolants from proofs. They benefit from close proof theoretic connections between interpolants and proofs, but require a theorem prover to produce proof objects in a format the interpolation procedure understands. It adds a dependency between interpolation procedures and proof formats of the automated theorem prover. Can the dependency on proof objects be relaxed for interpolant generation? Model-based interpolation generation relies on exchanging models of formulas and unsatisfiable cores. We develop an algorithm for model-based interpolation for the theory of quantifier-free integer linear arithmetic with uninterpreted functions. The setting extends previous results for linear real arithmetic and uninterpreted functions, but in contrast to the linear real case cannot rely on uniform interpolation.

Keyphrases: arithmetic, automated theorem proving, interpolation, SMT, Uninterpreted Functions

@Booklet{EasyChair:10000,
  author = {Nikolaj Bjorner and Arie Gurfinkel and Sharon Shoham and Yakir Vizel},
  title = {Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic},
  howpublished = {EasyChair Preprint no. 10000},

  year = {EasyChair, 2023}}