{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:15Z","timestamp":1763468115197},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642389764"},{"type":"electronic","value":"9783642389771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38977-1_23","type":"book-chapter","created":{"date-parts":[[2013,6,10]],"date-time":"2013-06-10T02:18:51Z","timestamp":1370830731000},"page":"308-314","source":"Crossref","is-referenced-by-count":4,"title":["A Language for Building Verified Software Components"],"prefix":"10.1007","author":[{"given":"Gregory","family":"Kulczycki","sequence":"first","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]},{"given":"Joan","family":"Krone","sequence":"additional","affiliation":[]},{"given":"Joseph E.","family":"Hollingsworth","sequence":"additional","affiliation":[]},{"given":"William F.","family":"Ogden","sequence":"additional","affiliation":[]},{"given":"Bruce W.","family":"Weide","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Bucci","sequence":"additional","affiliation":[]},{"given":"Charles T.","family":"Cook","sequence":"additional","affiliation":[]},{"given":"Svetlana V.","family":"Drachova-Strang","sequence":"additional","affiliation":[]},{"given":"Blair","family":"Durkee","sequence":"additional","affiliation":[]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[]},{"given":"Wayne","family":"Heym","sequence":"additional","affiliation":[]},{"given":"Dustin","family":"Hoffman","sequence":"additional","affiliation":[]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[]},{"given":"Yu-Shan","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Aditi","family":"Tagore","sequence":"additional","affiliation":[]},{"given":"Nighat","family":"Yasmin","sequence":"additional","affiliation":[]},{"given":"Diego","family":"Zaccai","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"23_CR1","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. JACM\u00a050(1), 63\u201369 (2003)","journal-title":"JACM"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st Verified Software Competition: Experience Report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"23_CR3","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., et al.: Reasoning About Software-Component Behavior. In: Frakes, W.B. (ed.) ICSR 2000. LNCS, vol.\u00a01844, pp. 266\u2013283. Springer, Heidelberg (2000)"},{"issue":"5","key":"23_CR4","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/s00165-010-0154-3","volume":"23","author":"M. Sitaraman","year":"2011","unstructured":"Sitaraman, M., Adcock, B., Avigad, J., Bronish, D., Bucci, B., Frazier, D., Friedman, H.M., Harton, H.K., Heym, W., Kirschenbaum, J., Krone, J., Smith, H., Weide, B.W.: Building a Push-Button RESOLVE Verifier: Progress and Challenges. Formal Aspects of Computing\u00a023(5), 607\u2013626 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"23_CR5","unstructured":"Adcock, B.: Working Towards the Verified Software Process. Ph. D. thesis, Computer Science and Engineering, The Ohio State University (2010)"},{"key":"23_CR6","unstructured":"Harton, H.K.: Mechanical and Modular Verification Condition Generation for Object-Based Software. Ph. D. Dissertation, Clemson University, 305 pages (2011)"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Cook, C.T., Harton, H.K., Smith, H., Sitaraman, M.: Specification engineering and modular verification using a web-integrated verifying compiler. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 1379\u20131382 (2012)","DOI":"10.1109\/ICSE.2012.6227243"},{"key":"23_CR8","unstructured":"Kulczycki, G.: Direct Reasoning. Ph. D. Dissertation, Clemson University, 183 pages (2004)"},{"key":"23_CR9","unstructured":"Smith, H.: Engineering Specifications and Mathematics for Verified Software. Ph. D. Dissertation, Clemson University, (to appear, 2013)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-04211-9_4","volume-title":"Formal Foundations of Reuse and Domain Engineering","author":"J. Kirschenbaum","year":"2009","unstructured":"Kirschenbaum, J., Adcock, B., Bronish, D., Smith, H., Harton, H., Sitaraman, M., Weide, B.W.: Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping? In: Edwards, S.H., Kulczycki, G. (eds.) ICSR 2009. LNCS, vol.\u00a05791, pp. 31\u201340. Springer, Heidelberg (2009)"},{"issue":"5","key":"23_CR11","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1109\/32.90445","volume":"17","author":"D.E. Harms","year":"1991","unstructured":"Harms, D.E., Weide, B.W.: 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":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-27705-4_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Kulczycki","year":"2012","unstructured":"Kulczycki, G., Smith, H., Harton, H., Sitaraman, M., Ogden, W.F., Hollingsworth, J.E.: The Location Linking Concept: A Basis for Verification of Code Using Pointers. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 34\u201349. Springer, Heidelberg (2012)"},{"issue":"5","key":"23_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R.A. DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social Processes and Proofs of Theorems and Programs. Comm. ACM\u00a022(5), 271\u2013280 (1979)","journal-title":"Comm. ACM"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Cook, C.T., Drachova, S., Sun, Y.-S., Sitaraman, M., Carver, J., Hollingsworth, J.E.: Specification and reasoning in SE Projects Using a Web IDE. In: Proceedings Conference on Software Engineering Education & Technology, CSEE&T (2013)","DOI":"10.1109\/CSEET.2013.6595254"}],"container-title":["Lecture Notes in Computer Science","Safe and Secure Software Reuse"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38977-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:22:35Z","timestamp":1557793355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38977-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389764","9783642389771"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38977-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}