NIL: learning nonlinear interpolants
From MaRDI portal
Publication:2305413
DOI10.1007/978-3-030-29436-6_11OpenAlexW2969437902MaRDI QIDQ2305413
Bohua Zhan, Deepak Kapur, Jie An, Naijun Zhan, Mingshuai Chen, Ji'an Wang
Publication date: 10 March 2020
Full work available at URL: https://arxiv.org/abs/1905.11625
program verificationsupport vector machines (SVMs)counterexample-guided learningnonlinear Craig interpolant
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Variant quantifier elimination
- Deciding polynomial-transcendental problems
- Semidefinite programming relaxations for semialgebraic problems
- Interpolants in nonlinear theories over the reals
- NIL: learning nonlinear interpolants
- Obtaining exact value by approximate computations
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
- On Interpolation and Symbol Elimination in Theory Extensions
- Generating Non-linear Interpolants by Semidefinite Programming
- Real root isolation for tame elementary functions
- Craig Interpolation in the Presence of Non-linear Constraints
- Predicate Abstraction for Program Verification
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- 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
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Interpolation and Symbol Elimination
- Tools and Algorithms for the Construction and Analysis of Systems
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Automatically Refining Abstract Interpretations
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Computer Aided Verification
This page was built for publication: NIL: learning nonlinear interpolants
