{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:13:34Z","timestamp":1742948014844,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"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-27705-4_19","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T17:18:06Z","timestamp":1327511886000},"page":"241-242","source":"Crossref","is-referenced-by-count":3,"title":["Our Experience with the CodeContracts Static Checker"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Logozzo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","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. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105\u2013118 (2011)","DOI":"10.1145\/1925844.1926399"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-18275-4_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 150\u2013168. Springer, Heidelberg (2011)"},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"2103","DOI":"10.1145\/1774088.1774531","volume-title":"SAC 2010: Proceedings of the 2010 ACM Symposium on Applied Computing","author":"M. F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: SAC 2010: Proceedings of the 2010 ACM Symposium on Applied Computing, pp. 2103\u20132110. ACM, New York (2010)"},{"key":"19_CR5","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Code Contracts (March 2009)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M. F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static Contract Checking with Abstract Interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"19_CR7","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":"19_CR8","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":"19_CR9","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: SAC, pp. 184\u2013188 (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Checking compatibility of bit sizes in floating point comparison operations. In: 3rd workshop on Numerical and Symbolic Abstract Domains. ENTCS (2011)","DOI":"10.1016\/j.entcs.2012.10.004"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T00:44:49Z","timestamp":1640565889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_19"}},"subtitle":["(Invited Tutorial)"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}