NIL: learning nonlinear interpolants

DOI10.1007/978-3-030-29436-6_11MaRDI QIDQ2305413zbMATH OpenOpenAlexFDO

Authors Mingshuai Chen, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan, Ji'an Wang

Publication date 10 March 2020

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

zbMATH Keywords

program verificationsupport vector machines (SVMs)counterexample-guided learningnonlinear Craig interpolant

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Generating non-linear interpolants by semidefinite programming
• Nonlinear Craig interpolant generation
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Interpolants in nonlinear theories over the reals
• Interpolation and model checking for nonlinear arithmetic

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 4009063 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
• Abstractions from proofs
• Automated Deduction – CADE-20
• Automatically Refining Abstract Interpretations
• Constraint Solving for Interpolation
• Craig interpolation in the presence of non-linear constraints
• Deciding polynomial-transcendental problems
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Generating non-linear interpolants by semidefinite programming
• Interpolant strength
• Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
• Interpolants in nonlinear theories over the reals
• Interpolation and SAT-based model checking.
• Interpolation and Symbol Elimination
• Interpolation in Local Theory Extensions
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• NIL: learning nonlinear interpolants
• Obtaining exact value by approximate computations
• Pattern recognition and machine learning.
• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Predicate abstraction for program verification
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Real root isolation for exp-log functions
• Real root isolation for tame elementary functions
• Semidefinite programming relaxations for semialgebraic problems
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Variant quantifier elimination

Cited in

(3)

• NIL: learning nonlinear interpolants
• Quantifier elimination and Craig interpolation: the quantitative way
• NPLIC: a machine learning approach to piecewise linear interface construction

Describes a project that uses

Uses Software

• LIBSVM
• PVS

This page was built for publication: NIL: learning nonlinear interpolants

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