{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:53Z","timestamp":1779087533601,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642182747","type":"print"},{"value":"9783642182754","type":"electronic"}],"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-18275-4_12","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T00:06:38Z","timestamp":1295222798000},"page":"150-168","source":"Crossref","is-referenced-by-count":36,"title":["Precondition Inference from Intermittent Assertions and Application to Contracts on Collections"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"11","key":"12_CR1","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/MC.2003.1244535","volume":"36","author":"K. Arnout","year":"2003","unstructured":"Arnout, K., Meyer, B.: Uncovering hidden contracts: The. NET example. IEEE Computer\u00a036(11), 48\u201355 (2003)","journal-title":"NET example. IEEE Computer"},{"key":"12_CR2","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"12_CR3","unstructured":"Barnett, M., F\u00e4hndrich, M., Garbervetsky, D., Logozzo, F.: Annotations for (more) precise points-to analysis. In: IWACO 2007, Stockholm U. and KTH (2007)"},{"key":"12_CR4","first-page":"2103","volume-title":"SAC 2010","author":"M. Barnett","year":"2010","unstructured":"Barnett, M., F\u00e4hndrich, M., Logozzo, F.: Embedded contract languages. In: SAC 2010, pp. 2103\u20132110. ACM, New York (2010)"},{"key":"12_CR5","first-page":"118","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"12_CR6","first-page":"46","volume-title":"PLDI 1993","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: PLDI 1993, pp. 46\u201355. ACM, New York (1993)"},{"key":"12_CR7","first-page":"289","volume-title":"36th POPL","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: 36th POPL, pp. 289\u2013300. ACM, New York (2009)"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/1542476.1542517","volume-title":"PLDI","author":"S. Chandra","year":"2009","unstructured":"Chandra, S., Fink, S., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: PLDI, pp. 363\u2013374. ACM, New York (2009)"},{"key":"12_CR9","unstructured":"Cousot, P.: M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes (in French). Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble (1978)"},{"key":"12_CR10","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications, ch. 10","author":"P. Cousot","year":"1981","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 10, pp. 303\u2013342. Prentice-Hall, Englewood Cliffs (1981)"},{"issue":"1-2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P. Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS\u00a0277(1-2), 47\u2013103 (2002)","journal-title":"TCS"},{"key":"12_CR12","first-page":"237","volume-title":"IFIP Conf. on Formal Description of Programming Concepts","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) IFIP Conf. on Formal Description of Programming Concepts, pp. 237\u2013277. North-Holland, Amsterdam (1977)"},{"key":"12_CR13","first-page":"269","volume-title":"6th POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269\u2013282. ACM, New York (1979)"},{"issue":"2-3","key":"12_CR14","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming\u00a013(2-3), 103\u2013179 (1992)","journal-title":"Journal of Logic Programming"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-45937-5_13","volume-title":"Compiler Construction","author":"P. Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Modular static program analysis. In: CC 2002. LNCS, vol.\u00a02304, pp. 159\u2013178. Springer, Heidelberg (2002)"},{"key":"12_CR16","volume-title":"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: POPL 2011. ACM, New York (2011)"},{"issue":"8","key":"12_CR17","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. Dijkstra","year":"1975","unstructured":"Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. CACM\u00a018(8), 453\u2013457 (1975)","journal-title":"CACM"},{"key":"12_CR18","volume-title":"FoVeOOS","author":"M. F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Clousot: Static contract checking with abstract interpretation. In: FoVeOOS. Springer, Heidelberg (2010)"},{"key":"12_CR19","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended Static Checking for Java. In: PLDI, pp. 234\u2013245. ACM, New York (2002)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-71316-6_18","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"key":"12_CR21","volume-title":"Flow Analysis of Computer Programs","author":"M. Hecht","year":"1977","unstructured":"Hecht, M.: Flow Analysis of Computer Programs. Elsevier, North-Holland (1977)"},{"issue":"7","key":"12_CR22","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J. King","year":"1976","unstructured":"King, J.: Symbolic execution and program testing. CACM\u00a019(7), 385\u2013394 (1976)","journal-title":"CACM"},{"key":"12_CR23","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1991","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1991)"},{"issue":"10","key":"12_CR24","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. IEEE Computer\u00a025(10), 40\u201351 (1992)","journal-title":"IEEE Computer"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78163-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Moy","year":"2008","unstructured":"Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 188\u2013202. Springer, Heidelberg (2008)"},{"key":"12_CR26","first-page":"59","volume-title":"Machine Intelligences","author":"D. Park","year":"1969","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. In: Meltzer, B., Michie, D. (eds.) Machine Intelligences, vol.\u00a05, pp. 59\u201378. Edinburgh University Press, Edinburgh (1969)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X. Rival","year":"2005","unstructured":"Rival, X.: Understanding the origin of alarms in astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 303\u2013319. Springer, Heidelberg (2005)"},{"key":"12_CR28","unstructured":"Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)"}],"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-18275-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T18:08:03Z","timestamp":1685902083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}