{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:21:56Z","timestamp":1725574916827},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642180699"},{"type":"electronic","value":"9783642180705"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-18070-5_2","type":"book-chapter","created":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T14:18:02Z","timestamp":1295101082000},"page":"10-30","source":"Crossref","is-referenced-by-count":54,"title":["Static Contract Checking with Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Manuel","family":"F\u00e4hndrich","sequence":"first","affiliation":[]},{"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","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.\u00a0410(46) (2009)","DOI":"10.1016\/j.tcs.2009.07.033"},{"key":"2_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":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-74792-5_7","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Burdy, L., Charles, J., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L., Pavlova, M., Requet, A.: JACK\u00a0\u2014\u00a0A Tool for Validation of Security and Behaviour of Java Applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol.\u00a04709, pp. 152\u2013174. Springer, Heidelberg (2007)"},{"key":"2_CR4","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: PLDI 2003 (2003)","DOI":"10.1145\/781131.781153"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-89330-1_2","volume-title":"Programming Languages and Systems","author":"L. Chen","year":"2008","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A Sound Floating-Point Polyhedra Abstract Domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 3\u201318. Springer, Heidelberg (2008)"},{"key":"2_CR6","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":"2_CR7","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.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM POPL 1979 (1979)","DOI":"10.1145\/567752.567778"},{"key":"2_CR9","first-page":"238","volume-title":"4th POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P. Cousot","year":"2008","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of Abstractions in the ASTR\u00c9E Static Analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 272\u2013300. Springer, Heidelberg (2008)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Contract precondition inference from intermittent assertions on collections. In: VMCAI 2011 (2011)","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"2_CR12","volume-title":"Proceeding of the 38 th ACM Symposium on Principles of Programming Languages (POPL 2011)","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceeding of the 38 th ACM Symposium on Principles of Programming Languages (POPL 2011). ACM Press, New York (January 2011)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978 (1978)","DOI":"10.1145\/512760.512770"},{"key":"2_CR14","first-page":"213","volume-title":"OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Matthew, J., Parkinson, J.: jStar: Towards practical verification for Java. In: OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, pp. 213\u2013226. ACM, New York (2008)"},{"key":"2_CR15","unstructured":"ECMA. Standard ECMA-355, Common Language Infrastructure (June 2006)"},{"key":"2_CR16","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Code Contracts (March 2009)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: ACM SAC 2010 (2010)","DOI":"10.1145\/1774088.1774531"},{"key":"2_CR18","volume-title":"OOPSLA 2008","author":"P. Ferrara","year":"2008","unstructured":"Ferrara, P., Logozzo, F., F\u00e4hndrich, M.: Safer unsafe code in.NET. In: OOPSLA 2008. ACM Press, New York (2008)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002 (2002)","DOI":"10.1145\/512529.512558"},{"key":"2_CR21","first-page":"338","volume-title":"32nd POPL","author":"D. Gopan","year":"2005","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: 32nd POPL, pp. 338\u2013350. ACM Press, New York (2005)"},{"key":"2_CR22","first-page":"235","volume-title":"35th POPL","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: 35th POPL, pp. 235\u2013246. ACM Press, New York (2008)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B. Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the veriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 304\u2013311. Springer, Heidelberg (2010)"},{"key":"2_CR24","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":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Inf.\u00a06 (1976)","DOI":"10.1007\/BF00268497"},{"issue":"1-3","key":"2_CR27","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/s00454-008-9050-5","volume":"39","author":"L. Khachiyan","year":"2008","unstructured":"Khachiyan, L., Boros, E., Borys, E., Elbassioni, K.M., Gurvich, V.: Generating all vertices of a polyhedron is hard. Discrete & Computational Geometry\u00a039(1-3), 174\u2013190 (2008)","journal-title":"Discrete & Computational Geometry"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-10672-9_24","volume-title":"Programming Languages and Systems","author":"V. Laviron","year":"2009","unstructured":"Laviron, V., Logozzo, F.: Refining Abstract Interpretation-Based Static Analyses with Hints. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 343\u2013358. Springer, Heidelberg (2009)"},{"key":"2_CR29","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":"2009","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.\u00a05403, pp. 229\u2013244. Springer, Heidelberg (2009)"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Logozzo, F.: Modular static analysis of object-oriented languages. Th\u00e8se de doctorat en informatique, \u00c9cole polytechnique (2004)","DOI":"10.1007\/3-540-44898-5_3"},{"key":"2_CR31","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.: 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":"2_CR32","doi-asserted-by":"crossref","unstructured":"F. Logozzo and M. F\u00e4hndrich. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: ACM SAC 2008 (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A. Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, p. 117. Springer, Heidelberg (2002)"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"2_CR35","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019, 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Min\u00e9","year":"2005","unstructured":"Min\u00e9, A.: Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 348\u2013363. Springer, Heidelberg (2005)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"2_CR38","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":"2_CR39","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.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664. Springer, Heidelberg (2003)"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-68863-1_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F.: VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 220\u2013239. Springer, Heidelberg (2008)"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013White Box Test Generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18070-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T22:09:13Z","timestamp":1559945353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18070-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180699","9783642180705"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18070-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}