Generating non-linear interpolants by semidefinite programming

DOI10.1007/978-3-642-39799-8_25MaRDI QIDQ2864839zbMATH OpenOpenAlexFDO

Authors Liyun Dai, Bican Xia, Naijun Zhan

Publication date 26 November 2013

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.4739

zbMATH Keywords

Craig interpolantPositivstellensatzprogram verificationsemidefinite programming

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Real algebraic sets (14P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semidefinite programming (90C22)

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.

Recommendations

• Nonlinear Craig interpolant generation
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Constraint solving for interpolation
• Constraint Solving for Interpolation
• Interpolants in nonlinear theories over the reals

Cited in

(11)

• Symbolic polytopes for quantitative interpolation and verification
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Nonlinear Craig interpolant generation
• NIL: learning nonlinear interpolants
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
• A survey of satisfiability modulo theory
• Nonlinear Interpolation and Total Variation Diminishing Schemes
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Barrier certificates revisited
• Interpolation and model checking for nonlinear arithmetic

This page was built for publication: Generating non-linear interpolants by semidefinite programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864839)