Metadata 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.

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.

an Entity references as follows:

Graph IRI	Count
http://ns.inria.fr/covid19/graph/entityfishing	11
http://ns.inria.fr/covid19/graph/articles	3

Faceted Search & Find service v1.13.91

This work is licensed under a Creative Commons Attribution-Share Alike 3.0 Unported License.
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)
Copyright © 2009-2024 OpenLink Software