{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:55:07Z","timestamp":1743090907721,"version":"3.40.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_16","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T07:29:29Z","timestamp":1326958169000},"page":"235-250","source":"Crossref","is-referenced-by-count":18,"title":["Donut Domains: Efficient Non-convex Domains for Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Khalil","family":"Ghorbal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gogul","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoto","family":"Maeda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A. Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, 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.\u00a06012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Static Analysis","author":"X. Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, \u00c9.: Inferring Min and Max Invariants Using Max-Plus Polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 189\u2013204. Springer, Heidelberg (2008)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Bagnara, R.: A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. In: Science of Computer Programming, pp. 2\u2013119 (1999)","DOI":"10.1016\/S0167-6423(97)00009-9"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Form. Asp. Comput., 222\u2013257 (2005)","DOI":"10.1007\/s00165-005-0061-1"},{"issue":"4-5","key":"16_CR5","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. STTT\u00a08(4-5), 449\u2013466 (2006)","journal-title":"STTT"},{"issue":"5","key":"16_CR6","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1016\/j.comgeo.2009.09.002","volume":"43","author":"R. Bagnara","year":"2010","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Exact join detection for convex polyhedra and other numerical abstractions. Comput. Geom.\u00a043(5), 453\u2013473 (2010)","journal-title":"Comput. Geom."},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0925-7721(03)00048-8","volume":"27","author":"A. Bemporad","year":"2004","unstructured":"Bemporad, A., Filippi, C., Torrisi, F.D.: Inner and outer approximations of polytopes using boxes. Comput. Geom.\u00a027(2), 151\u2013178 (2004)","journal-title":"Comput. Geom."},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0925-7721(01)00004-9","volume":"18","author":"A. Bemporad","year":"2001","unstructured":"Bemporad, A., Fukuda, K., Torrisi, F.D.: Convexity recognition of the union of polyhedra. Comput. Geom.\u00a018(3), 141\u2013154 (2001)","journal-title":"Comput. Geom."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: FMCAD, pp. 53\u201360. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351143"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-03237-0_21","volume-title":"Static Analysis","author":"L. Chen","year":"2009","unstructured":"Chen, L., Min\u00e9, A., Wang, J., Cousot, P.: Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 309\u2013325. Springer, Heidelberg (2009)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Intl. Symp. on Programming, Dunod, France, pp. 106\u2013130 (1976)","DOI":"10.1145\/390018.808314"},{"key":"16_CR12","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: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: POPL, pp. 84\u201397. ACM (January 1978)","DOI":"10.1145\/512760.512770"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-30579-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2005","unstructured":"Dams, D., Namjoshi, K.S.: Automata as Abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 216\u2013232. Springer, Heidelberg (2005)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/978-3-642-02658-4_47","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2009","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: The Zonotope Abstract Domain Taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 627\u2013633. Springer, Heidelberg (2009)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-14295-6_22","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2010","unstructured":"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.\u00a06174, pp. 212\u2013226. Springer, Heidelberg (2010)"},{"key":"16_CR17","unstructured":"Goldsztejn, A., Daney, D., Rueher, M., Taillibert, P.: Modal intervals revisited: a mean-value extension to generalized intervals. In: QCP (2005)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2006","unstructured":"Goubault, \u00c9., Putot, S.: Static Analysis of Numerical Algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 18\u201334. Springer, Heidelberg (2006)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-74061-2_9","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2007","unstructured":"Goubault, \u00c9., Putot, S.: Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 137\u2013152. Springer, Heidelberg (2007)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-53982-4_10","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"P. Granger","year":"1991","unstructured":"Granger, P.: Static Analysis of Linear Congruence Equalities Among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 169\u2013192. Springer, Heidelberg (1991)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-15769-1_18","volume-title":"Static Analysis","author":"A. Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: A Symbolic Abstract Domain of Boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 287\u2013303. Springer, Heidelberg (2010)"},{"key":"16_CR22","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: LeCharlier, B. (ed.) SAS 1994. LNCS, vol.\u00a0864, pp. 223\u2013237. Springer, Heidelberg (1994)"},{"key":"16_CR23","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.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-02658-4_33","volume-title":"Computer Aided Verification","author":"A. Kanade","year":"2009","unstructured":"Kanade, A., Alur, R., Ivan\u010di\u0107, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and Analyzing Symbolic Traces of Simulink\/Stateflow Models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 430\u2013445. Springer, Heidelberg (2009)"},{"key":"16_CR25","unstructured":"Makhorin, A.: The GNU Linear Programming Kit, GLPK (2000), http:\/\/www.gnu.org\/software\/glpk\/glpk.html"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Masdupuy, F.: Array abstractions using semantic analysis of trapezoid congruences. In: ICS, pp. 226\u2013235 (1992)","DOI":"10.1145\/143369.143414"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE, pp. 310\u2013319 (October 2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-642-22655-7_27","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"P. Prabhu","year":"2011","unstructured":"Prabhu, P., Maeda, N., Balakrishnan, G., Ivan\u010di\u0107, F., Gupta, A.: Interprocedural Exception Analysis for C++. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol.\u00a06813, pp. 583\u2013608. Springer, Heidelberg (2011)"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-69738-1_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. P\u00e9ron","year":"2007","unstructured":"P\u00e9ron, M., Halbwachs, N.: An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 268\u2013282. Springer, Heidelberg (2007)"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Rockafellar, R.T.: Convex Analysis. Princeton University Press (1970)","DOI":"10.1515\/9781400873173"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T23:25:01Z","timestamp":1742340301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}