Generating Non-linear Interpolants by Semidefinite Programming

DOI10.1007/978-3-642-39799-8_25zbMath1503.68181arXiv1302.4739OpenAlexW1792477536MaRDI QIDQ2864839

Naijun Zhan, Liyun Dai, Bican Xia

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

semidefinite programmingPositivstellensatzprogram verificationCraig interpolant

Mathematics Subject Classification ID

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

Related Items (9)

Interpolation and model checking for nonlinear arithmetic ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Barrier certificates revisited ⋮ Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ NIL: learning nonlinear interpolants ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ A Survey of Satisfiability Modulo Theory

This page was built for publication: Generating Non-linear Interpolants by Semidefinite Programming