{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:49Z","timestamp":1725537229544},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642042102"},{"type":"electronic","value":"9783642042119"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04211-9_4","type":"book-chapter","created":{"date-parts":[[2009,9,3]],"date-time":"2009-09-03T01:36:22Z","timestamp":1251941782000},"page":"31-40","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?"],"prefix":"10.1007","author":[{"given":"Jason","family":"Kirschenbaum","sequence":"first","affiliation":[]},{"given":"Bruce","family":"Adcock","sequence":"additional","affiliation":[]},{"given":"Derek","family":"Bronish","sequence":"additional","affiliation":[]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]},{"given":"Bruce W.","family":"Weide","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-44995-9_16","volume-title":"Software Reuse: Advances in Software Reusability","author":"M. Sitaraman","year":"2000","unstructured":"Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B.W., Long, T.J., Bucci, P., Heym, W.D., Pike, S.M., Hollingsworth, J.E.: Reasoning about software-component behavior. In: Frakes, W.B. (ed.) ICSR 2000. LNCS, vol.\u00a01844, pp. 266\u2013283. Springer, Heidelberg (2000)"},{"issue":"1","key":"4_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"issue":"5","key":"4_CR3","first-page":"661","volume":"13","author":"J. Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The verification grand challenge. Journal of Universal Computer Science\u00a013(5), 661\u2013668 (2007), http:\/\/www.jucs.org\/jucs_13_5\/the_verification_grand_challenge","journal-title":"Journal of Universal Computer Science"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Enderton, H.: A Mathematical Introduction to Logic. Harcourt\/Academic Press (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-87873-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"B.W. Weide","year":"2008","unstructured":"Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 84\u201398. Springer, Heidelberg (2008)"},{"issue":"4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/190679.190681","volume":"19","author":"W.F. Ogden","year":"1994","unstructured":"Ogden, W.F., Sitaraman, M., Weide, B.W., Zweben, S.H.: Part I: the RESOLVE framework and discipline: a research synopsis. SIGSOFT Softw. Eng. Notes\u00a019(4), 23\u201328 (1994)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1109\/32.90445","volume":"17","author":"D. Harms","year":"1991","unstructured":"Harms, D., Weide, B.: Copying and swapping: Influences on the design of reusable software components. IEEE Transactions on Software Engineering\u00a017(5), 424\u2013435 (1991)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR8","unstructured":"Krone, J.: The Role of Verification in Software Reusability. PhD thesis, Department of Computer and Information Science, The Ohio State University, Columbus, OH (December 1988)"},{"key":"4_CR9","unstructured":"Heym, W.D.: Computer Program Verification: Improvements for Human Reasoning. PhD thesis, Department of Computer and Information Science, The Ohio State University, Columbus, OH (December 1995)"},{"key":"4_CR10","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":"4_CR11","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":"4_CR12","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview, http:\/\/citeseer.ist.psu.edu\/649115.html"},{"key":"4_CR13","first-page":"82","volume-title":"PASTE 2005: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE 2005: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 82\u201387. ACM, New York (2005)"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1379022.1375624","volume":"43","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. SIGPLAN Not.\u00a043(6), 349\u2013361 (2008)","journal-title":"SIGPLAN Not."}],"container-title":["Lecture Notes in Computer Science","Formal Foundations of Reuse and Domain Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04211-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T06:27:02Z","timestamp":1558506422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04211-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042102","9783642042119"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04211-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}