Top

Published in:

2018 | OriginalPaper | Chapter

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints

Authors : Alexey Bakhirkin, David Monniaux

Published in: Static Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Block-Size Independence for GPU Programs

next chapter An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

Available only for authorised users

\(\mathrel {\rightarrow }\) denotes logical implication.

In the case of polyhedra with nonempty interior, an non-redundant system of normalized inequalities canonically describes a polyhedron: each inequality corresponds to a face. This is not true in the general case: both \(x \le y \wedge y \le x \wedge 0 \le x \wedge x \le 1\) and \(x \le y \wedge y \le x \wedge 0 \le x \wedge y \le 1\) are non-redundant systems defining the same polyhedron. Its affine span is defined by \(x=y\), then one can rewrite the inequalities using this equality and obtain \(x =y \wedge 0 \le y \wedge y \le 1\), which is canonical.

Competition on software verification (SV-COMP). http://sv-comp.sosy-lab.org/. Accessed Apr 2018

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA. IEEE (2009)

Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)MathSciNetCrossRef

Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT 9(3–4), 413–414 (2007)CrossRef

Bakhirkin, A.: HCAI, a path focusing abstract interpreter for Horn clauses. https://gitlab.com/abakhirkin/hcai. Accessed Apr 2018

Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. In: Ranzato [29], pp. 23–45

Benoy, F., King, A., Mesnard, F.: Computing convex hulls with a linear solver. TPLP 5(1–2), 259–271 (2005)MATH

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–32

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_2CrossRef

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–60

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_3CrossRef

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)

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)

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.

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_18CrossRef

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_20CrossRef

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.

Imbert, J.: Fourier’s elimination: which to choose? In: PPCP, pp. 117–129 (1993)

19.

Jeannet, B.: Bddapron. http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/bddapron/. Accessed Apr 2018

20.

Kohler, D.: Projections of convex polyhedral sets. Ph.D. thesis, University of California, Berkeley (1967)

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)

22.

Maréchal, A., Monniaux, D., Périn, M.: Scalable minimizing-operators on polyhedra via parametric linear programming. In: Ranzato [29], pp. 212–231

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_20CrossRef

24.

McMullen, P.: The maximum numbers of faces of a convex polytope. Mathematika 17, 179–184 (1970)MathSciNetCrossRef

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_13CrossRef

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_27CrossRef

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_18CrossRef

28.

Motzkin, T.S.: Beiträge zur Theorie der Linearen Ungleichungen. Ph.D. thesis, Universität Zürich (1936)

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)

30.

Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007)CrossRef

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_23CrossRefMATH

Title: Extending Constraint-Only Representation of Polyhedra with Boolean Constraints
Authors: Alexey Bakhirkin
David Monniaux
Publisher: Springer International Publishing
Book: Static Analysis
Print ISBN: 978-3-319-99724-7

Electronic ISBN: 978-3-319-99725-4

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-99725-4_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner