Advertisement

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints

  • Alexey BakhirkinEmail author
  • David Monniaux
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

We propose a new relational abstract domain for analysing programs with numeric and Boolean variables. The main idea is to represent an abstract state as a set of linear constraints over numeric variables, with every constraint being enabled by a formula over Boolean variables. This allows us, unlike in some existing approaches, to avoid duplicating linear constraints shared by multiple Boolean formulas. To perform domain operations, we adapt algorithms from constraint-only representation of convex polyhedra, most importantly Fourier-Motzkin elimination and projection-based convex hull. We made a prototype implementation of the new domain in our abstract interpreter for Horn clauses. Our initial experiments are, in our opinion, promising and show directions for future improvement.

Supplementary material

References

  1. 1.
    Competition on software verification (SV-COMP). http://sv-comp.sosy-lab.org/. Accessed Apr 2018
  2. 2.
    Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA. IEEE (2009)Google Scholar
  3. 3.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT 9(3–4), 413–414 (2007)CrossRefGoogle Scholar
  5. 5.
    Bakhirkin, A.: HCAI, a path focusing abstract interpreter for Horn clauses. https://gitlab.com/abakhirkin/hcai. Accessed Apr 2018
  6. 6.
    Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. In: Ranzato [29], pp. 23–45Google Scholar
  7. 7.
    Benoy, F., King, A., Mesnard, F.: Computing convex hulls with a linear solver. TPLP 5(1–2), 259–271 (2005)zbMATHGoogle Scholar
  8. 8.
    Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA [2], pp. 25–32Google Scholar
  9. 9.
    Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23534-9_2CrossRefGoogle Scholar
  10. 10.
    Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA [2], pp. 53–60Google Scholar
  11. 11.
    Chen, J., Cousot, P.: A binary decision tree abstract domain functor. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 36–53. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-48288-9_3CrossRefGoogle Scholar
  12. 12.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84–96. ACM Press (1978)Google Scholar
  13. 13.
    Fouilhé, A.: Revisiting the abstract domain of polyhedra : constraints-only representation and formal proof. (Le domaine abstrait des polyèdres revisité : représentation par contraintes et preuve formelle). Ph.D. thesis, Université Grenoble Alpes, France (2015)Google Scholar
  14. 14.
    Fourier, J.: Note, second extrait. Histoire de l’Académie pour 1824, p. xlvii, vol. 2, pp. 325–328. Gauthier-Villars, Paris (1890). http://gallica.bnf.fr/ark:/12148/bpt6k33707/f330
  15. 15.
    Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287–303. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_18CrossRefGoogle Scholar
  16. 16.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_20CrossRefGoogle Scholar
  17. 17.
    Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Ph.D. thesis, Université Scientifique et Médicale de Grenoble & Institut National Polytechnique de Grenoble, March 1979. https://tel.archives-ouvertes.fr/tel-00288805
  18. 18.
    Imbert, J.: Fourier’s elimination: which to choose? In: PPCP, pp. 117–129 (1993)Google Scholar
  19. 19.
    Jeannet, B.: Bddapron. http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/bddapron/. Accessed Apr 2018
  20. 20.
    Kohler, D.: Projections of convex polyhedral sets. Ph.D. thesis, University of California, Berkeley (1967)Google Scholar
  21. 21.
    Maréchal, A.: New Algorithmics for Polyhedral Calculus via Parametric Linear Programming. (Nouvelle Algorithmique pour le Calcul Polyédral via Programmation Linéaire Paramétrique). Ph.D. thesis, Université Grenoble Alpes, France (2017)Google Scholar
  22. 22.
    Maréchal, A., Monniaux, D., Périn, M.: Scalable minimizing-operators on polyhedra via parametric linear programming. In: Ranzato [29], pp. 212–231Google Scholar
  23. 23.
    Maréchal, A., Périn, M.: Efficient elimination of redundancies in polyhedra by raytracing. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 367–385. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_20CrossRefGoogle Scholar
  24. 24.
    McMullen, P.: The maximum numbers of faces of a convex polytope. Mathematika 17, 179–184 (1970)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Monniaux, D., Alberti, F.: A Simple abstraction of arrays and maps by program translation. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 217–234. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-48288-9_13CrossRefGoogle Scholar
  26. 26.
    Monniaux, D., Gonnord, L.: Using bounded model checking to focus fixpoint iterations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 369–385. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_27CrossRefGoogle Scholar
  27. 27.
    Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361–382. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53413-7_18CrossRefGoogle Scholar
  28. 28.
    Motzkin, T.S.: Beiträge zur Theorie der Linearen Ungleichungen. Ph.D. thesis, Universität Zürich (1936)Google Scholar
  29. 29.
    Ranzato, F. (ed.): Static Analysis - 24th International Symposium, SAS 2017,New York, NY, USA, August 30 - September 1, 2017, Proceedings, Lecture Notesin Computer Science, vol. 10422. Springer (2017)Google Scholar
  30. 30.
    Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007)CrossRefGoogle Scholar
  31. 31.
    Simon, A., King, A.: Exploiting sparsity in polyhedral analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005).  https://doi.org/10.1007/11547662_23CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAGGrenobleFrance

Personalised recommendations