About: Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. In this paper, we first prove that a polynomial interpolant of the form [Formula: see text] exists for two mutually contradictory polynomial formulas [Formula: see text] and [Formula: see text], with the form [Formula: see text], where [Formula: see text] are polynomials in [Formula: see text] or [Formula: see text], and the quadratic module generated by [Formula: see text] is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem ([Formula: see text]). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in [Formula: see text] solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.   Goto Sponge  NotDistinct  Permalink

An Entity of Type : fabio:Abstract, within Data Space : covidontheweb.inria.fr associated with source document(s)

AttributesValues
type
value
  • Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. In this paper, we first prove that a polynomial interpolant of the form [Formula: see text] exists for two mutually contradictory polynomial formulas [Formula: see text] and [Formula: see text], with the form [Formula: see text], where [Formula: see text] are polynomials in [Formula: see text] or [Formula: see text], and the quadratic module generated by [Formula: see text] is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem ([Formula: see text]). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in [Formula: see text] solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.
Subject
  • Video
  • Algebra
  • Concepts in physics
  • Dynamical systems
  • Nonlinear systems
  • Interpolation
  • Real algebraic geometry
  • Video signal
  • Polynomials
  • Electronic circuit verification
  • Ordered groups
part of
is abstract of
is hasSource of
Faceted Search & Find service v1.13.91 as of Mar 24 2020


Alternative Linked Data Documents: Sponger | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data]
OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software