Sharper and Simpler Nonlinear Interpolants for Program Verification

DOI10.1007/978-3-319-71237-6_24zbMath1503.68184arXiv1709.00314OpenAlexW2962939325MaRDI QIDQ5056007

Takamasa Okudono, Kohei Suenaga, Kengo Kido, Kensuke Kojima, Yuki Nishida, Ichiro Hasuo

Publication date: 9 December 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

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

zbMATH Keywords

interpolationpolynomialnumerical optimizationreal algebraic geometryprogram verificationnonlinear interpolantSDP optimization

Mathematics Subject Classification ID

Real algebraic sets (14P05) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Interpolation, preservation, definability (03C40)

Related Items (3)

Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis ⋮ NIL: learning nonlinear interpolants

Uses Software

• SDPT3
• Orbital library
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Barrier certificates revisited
• Semidefinite programming relaxations for semialgebraic problems
• Interpolants in nonlinear theories over the reals
• Computing sum of squares decompositions with rational coefficients
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Verification of positive definiteness
• A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
• Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
• Generating Non-linear Interpolants by Semidefinite Programming
• Craig Interpolation in the Presence of Non-linear Constraints
• Abstractions from proofs
• Counterexample-guided abstraction refinement for symbolic model checking
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Interpolation Properties and SAT-Based Model Checking
• Real World Verification
• Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars
• A Data Driven Approach for Algebraic Loop Invariants
• Constraint Solving for Interpolation
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Validating numerical semidefinite programming solvers for polynomial invariants

This page was built for publication: Sharper and Simpler Nonlinear Interpolants for Program Verification