{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:21:53Z","timestamp":1725574913187},"publisher-location":"Berlin, Heidelberg","reference-count":30,"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_11","type":"book-chapter","created":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T09:18:02Z","timestamp":1295083082000},"page":"153-167","source":"Crossref","is-referenced-by-count":5,"title":["A Refinement Methodology for Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Asma","family":"Tafat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Boulm\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book, assigning programs to meaning","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book, assigning programs to meaning. Cambridge University Press, Cambridge (1996)"},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"issue":"6","key":"11_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"11_CR5","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":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"11_CR7","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language (2008), http:\/\/frama-c.cea.fr\/acsl.html"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: A successful application of B in a large project. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/11955757_4","volume-title":"B 2007: Formal Specification and Development in B","author":"S. Boulm\u00e9","year":"2006","unstructured":"Boulm\u00e9, S., Potet, M.-L.: Interpreting invariant composition in the B method using the spec# ownership relation: A way to explain and relax B restrictions. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 4\u201318. Springer, Heidelberg (2006)"},{"key":"11_CR10","unstructured":"Breunesse, C.-B., Poll, E.: Verifying JML specifications with model fields. In: FTfJP 2003 (2003)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (2004)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"11_CR12","unstructured":"Charles, J.: Adding native specifications to JML. In: FTfJP 2006 (2006)"},{"issue":"6","key":"11_CR13","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exper.\u00a035(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Exper."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting eSC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"11_CR15","unstructured":"Darvas, A.P.: Reasoning About Data Abstraction in Contract Languages. PhD thesis, ETH Zurich (2009)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"11_CR17","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":"11_CR18","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. In: Formal Aspects of Computing (2007)","DOI":"10.1007\/s00165-007-0026-7"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA 1998, pp. 144\u2013153 (1998)","DOI":"10.1145\/286942.286953"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"issue":"5","key":"11_CR21","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Trans. Prog. Lang. Syst.\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"11_CR22","volume-title":"PLDI 2002","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: PLDI 2002. ACM, New York (2002)"},{"issue":"6","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst.\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR24","volume-title":"Programming from specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from specifications, 2nd edn. Prentice Hall International (UK) Ltd., Englewood Cliffs (1994)","edition":"2"},{"key":"11_CR25","unstructured":"Parkinson, M.: Class invariants: The end of the road. In: IWACO 2007 (2007), http:\/\/www.cs.purdue.edu\/homes\/wrigstad\/iwaco\/"},{"key":"11_CR26","volume-title":"17h Annual IEEE Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17h Annual IEEE Symposium on Logic in Computer Science. IEEE Comp. Soc. Press, Los Alamitos (2002)"},{"key":"11_CR27","unstructured":"Tafat, A., Boulm\u00e9, S., March\u00e9, C.: A refinement approach for correct-by-construction object-oriented programs. Technical Report RR-7310, INRIA (2010)"},{"issue":"3","key":"11_CR28","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0956796800000393","volume":"2","author":"J.-P. Talpin","year":"1992","unstructured":"Talpin, J.-P., Jouvelot, P.: Polymorphic type, region and effect inference. Journal of Functional Programming\u00a02(3), 245\u2013271 (1992)","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation\u00a0132(2), 109\u2013176 (1997)","journal-title":"Information and Computation"},{"key":"11_CR30","first-page":"349","volume-title":"PLDI 2008","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI 2008, pp. 349\u2013361. ACM Press, New York (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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:09:15Z","timestamp":1559930955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18070-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180699","9783642180705"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18070-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}