Generating Sharper and Simpler
Nonlinear Interpolants for Program Verification

Takamasa Okudono1, Yuki Nishida2, Kensuke Kojima2, Kohei Suenaga2, Kengo Kido1, and Ichiro Hasuo3
123

University of Tokyo, Japan; Kyoto University, Japan; National Institute of Informatics, Japan

Summary

Method for Sharpness (Cont’d)Parrilo’s Method

Method for Sharpness(1) Formulas

𝐴, 𝐵(6) Interpolant

𝐼Motivation(2) Polynomial
Optimization
Problem(3) SDP
Problem(5) Numerical
Solutionof (2)(4) Numerical
Solutionof (3)Use SDP Solver

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. [2] that combines real algebraic
geometry and SDP optimization in synthesis of polynomial interpolants, thecurrent 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 thatrounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool’s effectiveness; we also demonstrate the benefitof sharp and simple interpolants in program verification examples.

Figure 2: The Workflow of the Method for Sharpness

An interpolant I of formulas A and B that satisfy |= ¬(A ∧ B) satisfying (1)|= A → I, (2) |= ¬(I ∧ B) and (3) I contains only variables that appear bothin A and B.
I A polynomial interpolant is a variant of interpolants for the theory ofpolynomials.
IAtomic propositions are equalities (=), inequalities (≥) and strict inequalities (>) ofpolynomials.
I For example, a formula I = (y > 0) is an interpolant of A = (y > x ∧ y > −x) andB = (y ≤ 0) (See Figure 1, Input 1).
II

Polynomial interpolants are potentially useful for the verification ofpolynomial programs (imperative programs that support expressions withfinitely many additions and multiplications).
I

I

Method for Simplicity
The workflow is shown in Figure 3.
I Modifying “Method for Sharpness” to get the simplicity.
I Our main idea is “Assume that SDP solvers return a complicated solution thatis shifted from a simple solution by numerical error, and guess the original
simple solution by simplifying the complicated solution.”
I We use our simplification-of-ratio algorithm in the step (5) at Figure 3.
I

Our simplification-of-ratio algorithm takes depth parameter d and a ratio a1 : · · · : an thenreturns the d-th simplified ratio a10 : . . . , an0 .
00I By increasing d, the simplified ratio a : . . . , a gets faithful to the original ratio a1 : · · · : ann1and loses simplicity.
I For example, the simplifications of (46.7375 : 155.0975 : 60.1733) are(1 : 3 : 1) → (3 : 10 : 4) → (31 : 103 : 40) → (97 : 322 : 125) → . . . .
I The ratio of the coefficients of polynomials is sufficient to determine a formula, so we donot simplify the coefficients itself, but simplify the ratio (Vapnik’s principle).
I

Interpolants play an important role in CEGAR [1] (a method of predicate abstraction andprogram verification)

We found that the lack of two properties below is an obstacle of theverification in the manner of CEGAR with polynomial interpolants:

Sharpness:
I An interpolant I of A and B is sharp ⇐⇒ the region of A and B are “touching”.
I For example, A = (y > x ∧ y > −x) and B = (y ≤ 0) in Figure 1, Input 1 are“touching”.
I The method of Dai et al. [2] cannot generate any sharp interpolants.
I Simplicity:
I An interpolant is simple if it can be expressed with coefficients of fewer digits.
I For example, xa + 2ya ≥ 0 is simpler than1.86858 × 10−10 + 54.1800xa + 108.3601ya ≥ 0.
I The method of Dai et al. [2] tends to yield less simple interpolants.
II

The validity of the simplified solution is checked at (6) in Figure 3, so thegenerated interpolant at (8) is guaranteed to be a valid interpolant.
II

The method of Dai et al. [2] does not hold this property, so the generated interpolant could
be spurious.l

This is a best-effort method. That means, the validation at (5) in Figure 3
might fail and the method might return no interpolants even if there exists aninterpolant.
Maybe spurious…
(1) Formulas

𝐴, 𝐵Input 1

Input 2

Input 9Figure 1: Experiments. The blue, orange and green areas are for A, B, I, respectively.

(2) Polynomial
Optimization
Problem(3) SDP
Problemd := 1

Method for Sharpness(5) satisfies (3)Validity is guaranteed!

Method for Sharpness
The workflow is shown in Figure 2.
I The conversion from (1) to (2) in Figure 2 is based on this proposition:

Interpolant

𝐼

Let T and T be0

T =~,Y~ ) ≥ 0 , . . . , fs (X~,Y~)≥0 ,f1(X~,Y~ ) = 0 , . . . , hu (X~,Y~)=0h1(X~,Y~ ) > 0 , . . . , gt (X~,Y~)>0 ,g1(X0~,Z~ ) ≥ 0 , . . . , f 00 (X~,Z~) ≥ 0 ,f10(Xs~,Z~ ) = 0 , . . . , h0 0 (X~,Z~) = 0h10 (Xu~,Z~) > 0g10 (X!

~,Z~) > 0, . . . , gt00 (X,,(1)~ denotes the variables that occur in both of T , T 0.
where X
Assume there existf ∈ C(f1, . . . , fs , g1, . . . , gt ) , f 0 ∈ C(f10, . . . , fs00, g10 , . . . , gt00) ,000g ∈ SC(g1, . . . , gt ) , h ∈ I(h1, . . . , hu ) , and h ∈ I(h1, . . . , hu0)00
such that f + f + g + h + h = 0 .
(2)Then T and T 0 are disjoint. Moreover S := (f + g + h > 0) satisfies
0
the conditions of an interpolant of T and T , except for Condition 3.
I

Algebraic structure C, SC and I are cones, strict cones, and ideals,respectively.
~,Y~ ,Z~ ] is a subset of the polynomial ring that satisfies
I A strict cone S ⊂ R[X[f , g ∈ S =⇒ (f + g ∈ S ∧ fg ∈ S)] and R>0 ⊂ S.

I(6) Simplified
Solutionof (3)Method for Simplicity!

T =(7) Simplified
Solutionof (2)

Using this proposition enables us to generate sharp interpolants, which wasimpossible in the method of Dai et al. [2](5) d-th
Simplificationof (4)

No
Simplification(8) Simple
and VerifiedI(4) Numerical
Solutionof (3)

FAILFigure 3: The Workflow of the Method for Sharpness and Simplicity

References
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement for symbolic model checking.
J. ACM, 50(5):752–794, 2003.
Liyun Dai, Bican Xia, and Naijun Zhan.
Generating non-linear interpolants by semidefinite programming.
In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV
2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science,
pages 364–380. Springer, 2013.

Acknowledgement
Thanks are due to Eugenia Sironi and Gidon Ernst for their useful comments. T.O., K. Kido and I.H. are supported by JST ERATO HASUO Metamathematics
for Systems Design Project (No. JPMJER1603), and JSPS Grants-in-Aid No. 15KT0012 & 15K11984. K. Kojima is supported by JST CREST. K.S. issupported by JST PRESTO No. JPMJPR15E5 and JSPS Grants-in-Aid No. 15KT0012. K. Kido is supported by JSPS Grant-in-Aid for JSPS Research Fellows
No. 15J05580.