{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:43Z","timestamp":1725537223769},"publisher-location":"Berlin, Heidelberg","reference-count":27,"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_2","type":"book-chapter","created":{"date-parts":[[2009,9,3]],"date-time":"2009-09-03T01:36:22Z","timestamp":1251941782000},"page":"11-20","source":"Crossref","is-referenced-by-count":6,"title":["Generating Verified Java Components through RESOLVE"],"prefix":"10.1007","author":[{"given":"Hampton","family":"Smith","sequence":"first","affiliation":[]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[]},{"given":"David","family":"Frazier","sequence":"additional","affiliation":[]},{"given":"Raghuveer","family":"Mohan","sequence":"additional","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_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)"},{"key":"2_CR2","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., 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)"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","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. STTT\u00a07(3), 212\u2013232 (2005)","journal-title":"STTT"},{"key":"2_CR4","unstructured":"Weide, B.W., Heym, W.D.: Specification and Verification with References. In: Proc. SAVCBS, pp. 50\u201359 (2001)"},{"key":"2_CR5","unstructured":"Kulczycki, G.: Direct Reasoning, Ph. D. Dissertation, Clemson University (2004)"},{"issue":"4","key":"2_CR6","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/190679.190682","volume":"19","author":"S.H. Edwards","year":"1994","unstructured":"Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Part II: specifying components in RESOLVE. SIGSOFT Softw. Eng. Notes\u00a019(4), 29\u201339 (1994)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"2_CR7","volume-title":"Wiley Encyclopedia of Computer Science and Engineering","author":"H.K. Harton","year":"2008","unstructured":"Harton, H.K., Sitaraman, M., Krone, J.: Formal Program Verification. In: Wah, B. (ed.) Wiley Encyclopedia of Computer Science and Engineering, John Wiley & Sons, Chichester (2008)"},{"key":"2_CR8","unstructured":"Sitaraman, M., Adcock, B., Avigad, J., Bronish, D., Bucci, P., Frazier, D., Friedman, H.M., Harton, H., Heym, W., Kirschenbaum, J., Krone, J., Smith, H., Weide, B.W.: Building a Push-Button RESOLVE Verifier: Progress and Challenges. Technical Report RSRG-09-01, School of Computing, Clemson University, Clemson, SC (2009)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Kuncak, K., Rinard, M.: An Overview of the Jahob Analysis System: Project Goals and Current Status. In: Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, p. 323 (2006)","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"2_CR10","unstructured":"Wies, T.: Symbolic Shape Analysis. Master\u2019s thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (September 2004)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field Constraint Analysis. In: Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation (2006)","DOI":"10.1007\/11609773_11"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. ACM SIGPLAN 2002 Conference on Programming language Design and Implementation. Berlin, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM Software Engineering Notes\u00a031, 1\u201338 (2006)","journal-title":"ACM Software Engineering Notes"},{"key":"2_CR15","unstructured":"Poll, E., Kiniry, J., Cok, D.: Introduction to JML, http:\/\/secure.ucd.ie\/products\/opensource\/ESCJava2\/ESCTools\/papers\/CASSIS2004.pdf"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T.H., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, A., Schmitt, P.H.: The KeY tool. Software and System Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"issue":"1-2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa Tool for Certification of Java\/JavaCard Programs Annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-87873-5_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"P. Chalin","year":"2008","unstructured":"Chalin, P., James, P.R., Karabotsos, G.: JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 70\u201383. Springer, Heidelberg (2008)"},{"key":"2_CR20","unstructured":"Cok, D.: Adapting JML to generic types and Java 1.6. In: Proc. SAVCBS, pp. 27\u201335 (2008)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 19","author":"J. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Werner, D., Holger, H. (eds.) CAV 19. LNCS, vol.\u00a04510. Springer, Berlin (2007)"},{"key":"2_CR22","unstructured":"Ranise, S., Deharbe, D.: The haRVey decision procedure, http:\/\/www.loria.fr\/~ranise\/haRVey\/"},{"key":"2_CR23","unstructured":"Smith, H., Roche, K., Sitaraman, M., Krone, J., Ogden, W.F.: Integrating math units and proof checking for specification and verification. In: Proc. SAVCBS, pp. 59\u201366 (2008)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-27799-6_8","volume-title":"Software Reuse: Methods, Techniques, and Tools","author":"J.M. Hunt","year":"2004","unstructured":"Hunt, J.M., Sitaraman, M.: Enhancements - Enabling Flexible Feature and Implementation Selection. In: Bosch, J., Krueger, C. (eds.) ICOIN 2004 and ICSR 2004. LNCS, vol.\u00a03107, pp. 86\u2013100. Springer, Heidelberg (2004)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Leonard, D., Hallstrom, J., Sitaraman, M.: Injecting Rapid Feedback and Collaborative Reasoning in Teaching Specifications. In: Proc. ACM SIGCSE 2009 (2009)","DOI":"10.1145\/1508865.1509046"},{"key":"2_CR26","first-page":"252","volume-title":"Proc. 29th SIGCSE Technical Symposium on Computer Science Education","author":"T.J. Long","year":"2009","unstructured":"Long, T.J., Weide, B.W., Bucci, P., Gibson, D.S., Sitaraman, M., Hollingsworth, J.E., Edwards, S.H.: Providing Intellectual Focus To CS1\/CS2. In: Proc. 29th SIGCSE Technical Symposium on Computer Science Education, pp. 252\u2013256. ACM Press, New York (2009)"},{"key":"2_CR27","first-page":"601","volume-title":"Proc. ICSR 2001","author":"M. Sitaraman","year":"2001","unstructured":"Sitaraman, M., Long, T.J., Weide, B.W., Harner, J., Wang, C.: A Formal Approach to Component-Based Software Engineering: Education and Evaluation. In: Proc. ICSR 2001, pp. 601\u2013609. IEEE, Los Alamitos (2001)"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T06:26:58Z","timestamp":1558506418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04211-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042102","9783642042119"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04211-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}