{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:56Z","timestamp":1760202776603,"version":"3.41.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319997247"},{"type":"electronic","value":"9783319997254"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_11","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T17:45:50Z","timestamp":1535564750000},"page":"146-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["An Efficient Abstract Domain for Not Necessarily Closed Polyhedra"],"prefix":"10.1007","author":[{"given":"Anna","family":"Becchi","sequence":"first","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2012.09.003","volume":"287","author":"G Amato","year":"2012","unstructured":"Amato, G., Scozzari, F.: The abstract domain of parallelotopes. Electr. Notes Theor. Comput. Sci. 287, 17\u201328 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11547662_3","volume-title":"Static Analysis","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 3\u201318. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_3"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337\u2013354. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_19"},{"issue":"1\u20132","key":"11_CR4","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1\u20132), 28\u201356 (2005)","journal-title":"Sci. Comput. Program."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-24622-0_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bagnara","year":"2004","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135\u2013148. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_13"},{"issue":"2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/s00165-005-0061-1","volume":"17","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Formal Asp. Comput. 17(2), 222\u2013257 (2005)","journal-title":"Formal Asp. Comput."},{"issue":"4\/5","key":"11_CR7","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-005-0215-8","volume":"8","author":"R Bagnara","year":"2006","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Softw. Tools for Technol. Transf. 8(4\/5), 449\u2013466 (2006)","journal-title":"Softw. Tools for Technol. Transf."},{"issue":"1\u20132","key":"11_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"46","key":"11_CR9","doi-asserted-by":"publisher","first-page":"4672","DOI":"10.1016\/j.tcs.2009.07.033","volume":"410","author":"R Bagnara","year":"2009","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410(46), 4672\u20134691 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-009-0073-1","volume":"35","author":"R Bagnara","year":"2009","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Formal Meth. Syst. Des. 35(3), 279\u2013323 (2009)","journal-title":"Formal Meth. Syst. Des."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213\u2013229. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45789-5_17"},{"key":"11_CR12","unstructured":"Becchi, A., Zaffanella, E.: A conversion procedure for NNC polyhedra. CoRR, abs\/1711.09593 (2017)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 230\u2013248, Cham, 2018. Springer International Publishing. An extended version with proofs is available as\u00a0[12]","DOI":"10.1007\/978-3-319-96145-3_13"},{"key":"11_CR14","unstructured":"Birkhoff, G.: Lattice Theory, vol. 25. Colloquium Publications. American Mathematical Society, Providence (1967)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), pp. 196\u2013207, San Diego, USA (2003)","DOI":"10.1145\/781131.781153"},{"issue":"2","key":"11_CR16","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/0041-5553(65)90045-5","volume":"5","author":"NV Chernikova","year":"1965","unstructured":"Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Comput. Math. Math. Phys. 5(2), 228\u2013233 (1965)","journal-title":"U.S.S.R. Comput. Math. Math. Phys."},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2006.03.009","volume":"64","author":"R Claris\u00f3","year":"2007","unstructured":"Claris\u00f3, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115\u2013139 (2007)","journal-title":"Sci. Comput. Program."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Cortesi, A.: Widening operators for abstract interpretation. In: Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2008), pp. 31\u201340, Cape Town, South Africa (2008)","DOI":"10.1109\/SEFM.2008.20"},{"issue":"1","key":"11_CR19","first-page":"24","volume":"37","author":"A Cortesi","year":"2011","unstructured":"Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation. Comput. Lang. Syst. Struct. 37(1), 24\u201342 (2011)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238\u2013252, Los Angeles, USA (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55844-6_142"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84\u201396, Tucson, USA (1978)","DOI":"10.1145\/512760.512770"},{"issue":"1","key":"11_CR23","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.entcs.2010.09.006","volume":"267","author":"J Fulara","year":"2010","unstructured":"Fulara, J., Durnoga, K., Jakubczyk, K., Schubert, A.: Relational abstract domain of weighted hexagons. Electr. Notes Theor. Comput. Sci. 267(1), 59\u201372 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR24","unstructured":"Genov, B.: The convex hull problem in practice: improving the running time of the double description method. Ph.D. thesis, University of Bremen, Germany (2014)"},{"key":"11_CR25","unstructured":"Halbwachs, N.: D\u00e9termination Automatique de Relations Lin\u00e9aires V\u00e9rifi\u00e9es par les Variables d\u2019un Programme. Th\u00e8se de 3\u00e8me cycle d\u2019informatique, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France (1979)"},{"issue":"1","key":"11_CR26","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10703-006-0013-2","volume":"29","author":"N Halbwachs","year":"2006","unstructured":"Halbwachs, N., Merchat, D., Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations. Formal Meth. Syst. Des. 29(1), 79\u201395 (2006)","journal-title":"Formal Meth. Syst. Des."},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-44898-5_20","volume-title":"Static Analysis","author":"N Halbwachs","year":"2003","unstructured":"Halbwachs, N., Merchat, D., Parent-Vigouroux, C.: Cartesian factoring of polyhedra in linear relation analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 355\u2013365. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_20"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis","author":"N Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223\u2013237. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58485-4_43"},{"issue":"2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Meth. Syst. Des. 11(2), 157\u2013185 (1997)","journal-title":"Formal Meth. Syst. Des."},{"key":"11_CR30","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-04761-9_23","volume-title":"Automated Technology for Verification and Analysis","author":"JM Howe","year":"2009","unstructured":"Howe, J.M., King, A.: Logahedra: a new weakly relational domain. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_23"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"issue":"3","key":"11_CR33","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/S0925-7721(02)00103-7","volume":"23","author":"V Kaibel","year":"2002","unstructured":"Kaibel, V., Pfetsch, M.E.: Computing the face lattice of a polytope from its vertex-facet incidences. Comput. Geom. 23(3), 281\u2013290 (2002)","journal-title":"Comput. Geom."},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-93900-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Laviron","year":"2008","unstructured":"Laviron, V., Logozzo, F.: SubPolyhedra: a (More) scalable approach to infer linear inequalities. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229\u2013244. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_20"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Proceedings of the 2008 ACM Symposium on Applied Computing, pp. 184\u2013188, Fortaleza, Brazil (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering, pp. 310\u2013319, Stuttgart, Germany (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"11_CR38","unstructured":"Min\u00e9, A.: Weakly relational numerical abstract domains. Ph.D. thesis, \u00c9cole Polytechnique, Paris, France (2005)"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Contributions to the Theory of Games - Volume II, Number 28 in Annals of Mathematics Studies, pp. 51\u201373, Princeton, USA (1953)","DOI":"10.1515\/9781400881970-004"},{"key":"11_CR40","unstructured":"Notani, V., Giacobazzi, R.: Learning based widening. In: 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017), New York, USA (2017)"},{"key":"11_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25\u201341. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_2"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Shaham, R., Kolodner, E.K., Sagiv, S.: Heap profiling for space-efficient Java. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 104\u2013113, Snowbird, USA (2001)","DOI":"10.1145\/378795.378820"},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/3-540-45013-0_7","volume-title":"Logic Based Program Synthesis and Transformation","author":"A Simon","year":"2003","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71\u201389. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45013-0_7"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Making numerical program analysis fast. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 303\u2013313, Portland, USA (2015)","DOI":"10.1145\/2813885.2738000"},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 46\u201359, Paris, France (2017)","DOI":"10.1145\/3009837.3009885"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: A practical construction for decomposing numerical abstract domains. PACMPL, 2(POPL), 55:1\u201355:28 (2018)","DOI":"10.1145\/3158143"},{"key":"11_CR47","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.entcs.2018.03.004","volume":"334","author":"E Zaffanella","year":"2018","unstructured":"Zaffanella, E.: On the efficiency of convex polyhedra. Electr. Notes Theor. Comput. Sci. 334, 31\u201344 (2018)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T17:25:26Z","timestamp":1751822726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}