Sharper and Simpler Nonlinear Interpolants for Program Verification
From MaRDI portal
interpolationnonlinear interpolantnumerical optimizationpolynomialprogram verificationreal algebraic geometrySDP optimization
Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Real algebraic sets (14P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Abstract: Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent result by Dai et al. that combines real algebraic geometry and SDP optimization in synthesis of polynomial interpolants, the current paper contributes its enhancement that yields sharper and simpler interpolants. The enhancement is made possible by: theoretical observations in real algebraic geometry; and our continued fraction-based algorithm that rounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool's effectiveness; we also demonstrate the benefit of sharp and simple interpolants in program verification examples.
Recommendations
Cites work
- A data driven approach for algebraic loop invariants
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- Abstractions from proofs
- Barrier certificates revisited
- Computer Aided Verification
- Computer Aided Verification
- Computing sum of squares decompositions with rational coefficients
- Constraint Solving for Interpolation
- Counterexample-guided abstraction refinement for symbolic model checking
- Craig interpolation in the presence of non-linear constraints
- Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Generating non-linear interpolants by semidefinite programming
- scientific article; zbMATH DE number 4029737 (Why is no real title available?)
- scientific article; zbMATH DE number 527343 (Why is no real title available?)
- scientific article; zbMATH DE number 783633 (Why is no real title available?)
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Interpolants in nonlinear theories over the reals
- Interpolation and SAT-based model checking.
- Interpolation Properties and SAT-Based Model Checking
- Lazy Abstraction with Interpolants
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- Real World Verification
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- Semidefinite programming relaxations for semialgebraic problems
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Validating numerical semidefinite programming solvers for polynomial invariants
- Verification of positive definiteness
- Verifying Nonlinear Real Formulas Via Sums of Squares
Cited in
(6)- Symbolic polytopes for quantitative interpolation and verification
- Nonlinear Craig interpolant generation
- NIL: learning nonlinear interpolants
- Generating non-linear interpolants by semidefinite programming
- scientific article; zbMATH DE number 7364137 (Why is no real title available?)
- Sharper and Simpler Nonlinear Interpolants for Program Verification
This page was built for publication: Sharper and Simpler Nonlinear Interpolants for Program Verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5056007)
