Skip to main content
SpringerLink
Log in

Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants

  • Conference paper
  • First Online:
Software Verification (NSV 2020, VSTTE 2020)

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

  • 295 Accesses

Abstract

We propose to extend an existing framework combining abstract interpretation and continuous constraint programming for numerical invariant synthesis, by using more expressive underlying abstract domains, such as zonotopes. The original method, which relies on iterative refinement, splitting and tightening a collection of abstract elements until reaching an inductive set, was initially presented in combination with simple underlying abstract elements: boxes and octagons. The novelty of our work is to use zonotopes, a sub-polyhedric domain that shows a good compromise between cost and precision. As zonotopes are not closed under intersection, we had to extend the existing framework, in addition to designing new operations on zonotopes, such as a novel splitting algorithm based on paving zonotopes by sub-zonotopes and parallelotopes. We implemented this method on top of the APRON library, and tested it on programs with non-linear loops that present complex, possibly non-convex, invariants. We present some results demonstrating both the interest of this splitting-based algorithm to synthesize invariants on such programs, and the good compromise presented by its use in combination with zonotopes with respect to its use with both simpler domains such as boxes and octagons, and more expressive domains such as polyhedra.

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.

    https://github.com/bibekkabi/taylor1plus.

  2. 2.

    https://github.com/bibekkabi/Prototype_analyzerwithApron.

  3. 3.

    https://github.com/bibekkabi/Prototype_analyzerwithApron/tree/master/NSV_files.

  4. 4.

    https://github.com/sosy-lab/sv-benchmarks/tree/master/c/floats-cdfpl.

References

  1. Miné, A., Breck, J., Reps, T.: An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 560–588. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_22

    Chapter  Google Scholar 

  2. Goubault, E., Putot, S.: A Zonotopic framework for functional abstractions. Formal Methods Syst. Des. 47(3), 302–360 (2016). https://doi.org/10.1007/s10703-015-0238-z

    Article  MATH  Google Scholar 

  3. Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69–87. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_5

    Chapter  Google Scholar 

  4. Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: automating abstract interpretation. Electron. Notes Theoret. Comput. Sci. 311, 15–32 (2015)

    Article  MathSciNet  Google Scholar 

  5. Ghorbal, K., Goubault, E., Putot, S.: The Zonotope abstract domain Taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_47

    Chapter  Google Scholar 

  6. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238–252. ACM (1977)

    Google Scholar 

  8. Stolfi, J., De Figueiredo, L.H.: Self-validated numerical methods and applications. In: Monograph for 21st Brazilian Mathematics Colloquium, IMPA (1997)

    Google Scholar 

  9. Le, V.T.H., Stoica, C., Alamo, T., Camacho, E.F., Dumur, D.: Zonotope-based set-membership estimation for multi-output uncertain systems. In: IEEE International Symposium on Intelligent Control (ISIC), pp. 212–217. IEEE (2013)

    Google Scholar 

  10. Tabatabaeipour, S.M., Stoustrup, J.: Set-membership state estimation for discrete time piecewise affine systems using Zonotopes. In: European Control Conference (ECC), pp. 3143–3148. IEEE (2013)

    Google Scholar 

  11. Girard, A., Le Guernic, C.: Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78929-1_16

    Chapter  MATH  Google Scholar 

  12. Combastel, C., Zhang, Q., Lalami, A.: Fault diagnosis based on the enclosure of parameters estimated with an adaptive observer. IFAC Proc. Volumes 41(2), 7314–7319 (2008)

    Article  Google Scholar 

  13. Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to Zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212–226. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_22

    Chapter  Google Scholar 

  14. Althoff, M., Krogh, B.H.: Zonotope bundles for the efficient computation of reachable sets. In: 50th IEEE Conference on Decision and Control and European Control Conference, pp. 6814–6821. IEEE (2011)

    Google Scholar 

  15. Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 297–306. ACM (2016)

    Google Scholar 

  16. Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Proceedings of the ACM-SIAM Symposium on Discrete Algorithms, pp. 803–812 (2003)

    Google Scholar 

  17. Bailey, G.D.: Tilings of Zonotopes: Discriminantal Arrangements. University of Minnesota, Oriented Matroids and Enumeration (1997)

    Google Scholar 

  18. Richter-Gebert, J., Ziegler, G.M.: Zonotopal tilings and the Bohne-Dress theorem. Contemp. Math. 178, 211 (1994)

    Article  MathSciNet  Google Scholar 

  19. Ferrez, J.A., Fukuda, K., Liebling, T.M.: Solving the fixed rank convex quadratic maximization in binary variables by a parallel Zonotope construction algorithm. Eur. J. Oper. Res. 166(1), 35–50 (2005)

    Article  MathSciNet  Google Scholar 

  20. Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_3

    Chapter  Google Scholar 

  21. Roux, P., Garoche, P.-L.: Practical policy iterations. Formal Methods Syst. Des. 46(2), 163–196 (2015). https://doi.org/10.1007/s10703-015-0230-7

    Article  MATH  Google Scholar 

  22. D’Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48–63. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_5

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

This work is being supported by project ANR-15-CE25-0002-01 COVERIF

Author information

Authors and Affiliations

  1. LIX, Ecole Polytechnique, CNRS, Institut Polytechnique de Paris, Palaiseau, France

    Bibek Kabi, Eric Goubault & Sylvie Putot

  2. Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, Paris, France

    Antoine Miné

Authors
  1. Bibek Kabi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eric Goubault
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antoine Miné
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sylvie Putot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvie Putot .

Editor information

Editors and Affiliations

  1. MPI-SWS Kaiserslautern, Kaiserslautern, Germany

    Maria Christakis

  2. University of California, San Diego, La Jolla, CA, USA

    Nadia Polikarpova

  3. Computer Science, University of North Carolina at Chapel Hill, Chapel Hill, NC, USA

    Parasara Sridhar Duggirala

  4. Engineering and Informatics, University of Sussex, Brighton, UK

    Peter Schrammel

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kabi, B., Goubault, E., Miné, A., Putot, S. (2020). Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds) Software Verification. NSV VSTTE 2020 2020. Lecture Notes in Computer Science(), vol 12549. Springer, Cham. https://doi.org/10.1007/978-3-030-63618-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-63618-0_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-63617-3

  • Online ISBN: 978-3-030-63618-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation