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
semi-definite programminginterpolantprogram verificationMotzkin's theoremSOSconcave quadratic polynomial
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)
Uses Software
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