Skip to main content
SpringerLink
Log in

Sharper and Simpler Nonlinear Interpolants for Program Verification

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10695))

Included in the following conference series:

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 effectiandveness; we also demonstrate the benefit of sharp and simple interpolants in program verification examples.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In Algorithm 2 we introduced the constraint \(\sum _{k\in \mathbf {b}^{t}}\gamma _k \ge 1\) in (13) as a relaxation of a natural constraint \(\sum _{k\in \mathbf {b}^{t}}\gamma _k > 0\); see Sect. 3.2. In the validation phase of our implementation we wind back the relaxation \(\sum _{k\in \mathbf {b}^{t}}\gamma _k \ge 1\) to the original constraint with \(>0\).

  2. 2.

    An interpolant \(716.77+1326.74(ya)+1.33(ya)^2+ 433.90(ya)^3+668.16(xa)-155.86(xa)(ya)+317.29(xa)(ya)^2+222.00(xa)^2+ 592.39(xa)^2(ya)+271.11(xa)^3 > 0\) is given in [8]. We note that, to show disjointness of \(\mathcal {T}\) and \(\mathcal {T}'\), an interpolant of any splitting of \(\mathcal {T} \cup \mathcal {T}'\) would suffice. It is not specified [8] which splitting they used.

  3. 3.

    Here we use a path-based CEGAR workflow that uses an execution path as a counterexample. Since we do not have any abstraction predicates, xa and ya can be any integer; in this case the assertion in Line 16 can potentially fail.

References

  1. Anai, H., Parrilo, P.A.: Convex quantifier elimination for semidefinite programming. In: Proceedings of the International Workshop on Computer Algebra in Scientific Computing, CASC (2003)

    Google Scholar 

  2. Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74464-1_4

    Chapter  Google Scholar 

  3. Bochnak, J., Coste, M., Roy, M.F.: Real Algebraic Geometry. Springer, New York (1999)

    MATH  Google Scholar 

  4. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003). https://doi.org/10.1145/876638.876643

    Article  MathSciNet  MATH  Google Scholar 

  5. Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., Somenzi [14], pp. 420–432

    Google Scholar 

  6. Dai, L.: The tool \(\mathtt{{aiSat}}\). github.com/djuanbei/aiSat. Accessed 17 Jan 2017

  7. Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62–86 (2017). https://doi.org/10.1016/j.jsc.2016.07.010

    Article  MathSciNet  MATH  Google Scholar 

  8. Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364–380. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_25

    Chapter  Google Scholar 

  9. Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 195–212. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_14

    Google Scholar 

  10. Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625–641. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_41

    Chapter  Google Scholar 

  11. Gurfinkel, A., Rollini, S.F., Sharygina, N.: Interpolation properties and SAT-based model checking. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 255–271. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_19

    Chapter  Google Scholar 

  12. Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102–118. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_9

    Chapter  Google Scholar 

  13. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14–16, 2004. pp. 232–244. ACM (2004). http://dl.acm.org/citation.cfm?id=964001

  14. Hunt Jr., W.A., Somenzi, F. (eds.): CAV 2003. LNCS, vol. 2725. Springer, Heidelberg (2003). https://doi.org/10.1007/b11831

    Google Scholar 

  15. Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_6

    Chapter  Google Scholar 

  16. Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_33

    Chapter  Google Scholar 

  17. Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In: Sendra, J.R., González-Vega, L. (eds.) Symbolic and Algebraic Computation, International Symposium, ISSAC 2008, Linz/Hagenberg, Austria, July 20–23, 2008, Proceedings, pp. 155–164. ACM (2008). http://doi.acm.org/10.1145/1390768.1390792

  18. Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240–255. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24310-3_17

    Chapter  Google Scholar 

  19. Lang, S.: Introduction to Diophantine Approximations. Springer Books on Elementary mathematics. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4220-8

    Book  MATH  Google Scholar 

  20. Lin, W., Wu, M., Yang, Z., Zeng, Z.: Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods. Front. Comput. Sci. 8(2), 192–202 (2014). https://doi.org/10.1007/s11704-014-3150-6

    Article  MathSciNet  Google Scholar 

  21. McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., Somenzi [14], pp. 1–13

    Google Scholar 

  22. McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_1

    Chapter  Google Scholar 

  23. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_14

    Chapter  Google Scholar 

  24. Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I.: Sharper and simpler nonlinear interpolants for program verification. CoRR abs/1709.00314 (2017)

    Google Scholar 

  25. Parrilo, P.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph.D. thesis, California Inst. of Tech. (2000)

    Google Scholar 

  26. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003). https://doi.org/10.1007/s10107-003-0387-5

    Article  MathSciNet  MATH  Google Scholar 

  27. Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theor. Comput. Sci. 409(2), 269–281 (2008). https://doi.org/10.1016/j.tcs.2008.09.025

    Article  MathSciNet  MATH  Google Scholar 

  28. Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_35

    Chapter  Google Scholar 

  29. Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. Journ. 42(3), 969–984 (1993)

    Article  MATH  Google Scholar 

  30. Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 424–446. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_21

    Chapter  Google Scholar 

  31. Rump, S.: Verification of positive definiteness. BIT Numer. Math. 46(2), 433–452 (2006). https://doi.org/10.1007/s10543-006-0056-1

    Article  MathSciNet  MATH  Google Scholar 

  32. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69738-1_25

    Chapter  Google Scholar 

  33. Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574–592. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_31

    Chapter  Google Scholar 

  34. Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87–97 (1974). https://doi.org/10.1007/BF01362149

    Article  MathSciNet  MATH  Google Scholar 

  35. Terauchi, T.: Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 128–144. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_8

    Chapter  Google Scholar 

  36. Toh, K.C., Todd, M., Tütüncü, R.H.: Sdpt3 - a matlab software package for semidefinite programming. Optim. Methods Softw. 11, 545–581 (1999)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

Thanks are due to Eugenia Sironi, Gidon Ernst and the anonymous referees 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. is supported 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.

Author information

Authors and Affiliations

  1. University of Tokyo, Tokyo, Japan

    Takamasa Okudono & Kengo Kido

  2. Kyoto University, Kyoto, Japan

    Yuki Nishida, Kensuke Kojima & Kohei Suenaga

  3. JST PRESTO, Kyoto, Japan

    Kohei Suenaga

  4. JSPS Research Fellow, Tokyo, Japan

    Kengo Kido

  5. National Institute of Informatics, Tokyo, Japan

    Ichiro Hasuo

Authors
  1. Takamasa Okudono
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yuki Nishida
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kensuke Kojima
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kohei Suenaga
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Kengo Kido
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Ichiro Hasuo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Takamasa Okudono .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I. (2017). Sharper and Simpler Nonlinear Interpolants for Program Verification. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

  • Online ISBN: 978-3-319-71237-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation