{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T17:04:34Z","timestamp":1751648674595},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540938996"},{"type":"electronic","value":"9783540939009"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_20","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T09:35:59Z","timestamp":1229333759000},"page":"229-244","source":"Crossref","is-referenced-by-count":41,"title":["SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Laviron","sequence":"first","affiliation":[]},{"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","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.\u00a072(1) (2008)","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for Object-Oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"20_CR3","unstructured":"Barnett, M., F\u00e4hndrich, M., Logozzo, F.: Managed contract tools, http:\/\/research.microsoft.com\/downloads"},{"key":"20_CR4","unstructured":"Barnett, M., F\u00e4hndrich, M.A., Logozzo, F.: Foxtrot and Clousot: Language agnostic dynamic and static contract checking for. Net. Technical Report MSR-TR-2008-105, Microsoft Research (2008)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: APLAS 2008 (2008)","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"20_CR6","volume-title":"Linear Programming","author":"V. Chv\u00e1tal","year":"1983","unstructured":"Chv\u00e1tal, V.: Linear Programming. W.H. Freeman, New York (1983)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-540-27864-1_23","volume-title":"Static Analysis","author":"R. Claris\u00f3","year":"2004","unstructured":"Claris\u00f3, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 312\u2013327. Springer, Heidelberg (2004)"},{"key":"20_CR8","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"20_CR9","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 1977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979 (1979)","DOI":"10.1145\/567752.567778"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978 (1978)","DOI":"10.1145\/512760.512770"},{"key":"20_CR12","unstructured":"Dantzig, G.B.: Programming in linear structures. Technical report, USAF (1948)"},{"key":"20_CR13","unstructured":"Feret, J.: Analysis of mobile systems by abstract interpretation. PhD thesis"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Ferrara, P., Logozzo, F., F\u00e4hndrich, M.A.: Safer unsafe code in. Net. In: OOPSLA 2008 (2008)","DOI":"10.1145\/1449764.1449791"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K., Chilimbi, T.: Speed: Precise and efficient static estimation of program computational complexity. In: POPL 2009 (2009)","DOI":"10.1145\/1594834.1480898"},{"issue":"2","key":"20_CR17","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: On affine relationships among variables of a program. Acta Informatica\u00a06(2), 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Khachiyan, L., Boros, E., Borys, K., Elbassioni, K.M., Gurvich, M.: Generating all vertices of a polyhedron is hard. In: SODA 2006 (2006)","DOI":"10.1145\/1109557.1109640"},{"key":"20_CR19","unstructured":"Laviron, V., Logozzo, F.: The Subpoly Library, http:\/\/research.microsoft.com\/downloads"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-69738-1_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Logozzo","year":"2007","unstructured":"Logozzo, F.: Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of java classes. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 283\u2013298. Springer, Heidelberg (2007)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-78791-4_14","volume-title":"Compiler Construction","author":"F. Logozzo","year":"2008","unstructured":"Logozzo, F., F\u00e4hndrich, M.A.: On the relative completeness of bytecode analysis versus source code analysis. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 197\u2013212. Springer, Heidelberg (2008)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.A.: Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In: SAC 2008 (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"20_CR23","series-title":"Professional Technical Reference","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Professional Technical Reference. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"20_CR24","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE 2001 (2001)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL 2004 (2004)","DOI":"10.1145\/964001.964029"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program.\u00a064(1) (2007)","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-74061-2_23","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2007","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis using symbolic ranges. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 366\u2013383. Springer, Heidelberg (2007)"},{"key":"20_CR28","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.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Two variables per linear inequality as an abstract domain. In: Leuschel, M.A. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664. Springer, Heidelberg (2003)"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Spielman, D.A., Teng, S.-H.: Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time. J. ACM.\u00a051(3) (2004)","DOI":"10.1145\/990308.990310"}],"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-540-93900-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T08:11:43Z","timestamp":1557994303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}