Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF

DOI10.1007/978-3-319-40229-1_14zbMath1475.03072arXiv1601.04802OpenAlexW2295030121MaRDI QIDQ2817919

Mingshuai Chen, Deepak Kapur, Bican Xia, Liyun Dai, Ting Gan, Naijun Zhan

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

semi-definite programminginterpolantprogram verificationMotzkin's theoremSOSconcave quadratic polynomial

Mathematics Subject Classification ID

Semidefinite programming (90C22) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Related Items (4)

Interpolation and model checking for nonlinear arithmetic ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ NIL: learning nonlinear interpolants

Uses Software

• SDPT3
• CSIsat
• FOCI

Cites Work

• Unnamed Item
• Unnamed Item
• Solving semidefinite-quadratic-linear programs using SDPT3
• Barrier certificates revisited
• Constraint solving for interpolation
• Semidefinite programming relaxation for nonconvex quadratic programs
• A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
• An interpolating theorem prover
• Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
• Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants
• Generating Non-linear Interpolants by Semidefinite Programming
• Abstractions from proofs
• Interpolation in local theory extensions
• Interpolant Strength
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example
• Interpolation and Symbol Elimination
• Automated Deduction – CADE-20
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Computer Aided Verification

This page was built for publication: Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF