{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:03:17Z","timestamp":1791061397870,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288906","type":"print"},{"value":"9783642288913","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_30","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"310-325","source":"Crossref","is-referenced-by-count":5,"title":["Generating Verifiable Java Code from Verified PVS Specifications"],"prefix":"10.1007","author":[{"given":"Leonard","family":"Lensink","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling (2005)","DOI":"10.1007\/s10270-004-0058-x"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bailey, R., Hostetler, R., Barnes, K., Belcastro, C., Belcastro, C.: Experimental validation subscale aircraft ground facilities and integrated test capability. In: Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2005, San Francisco, California (2005)","DOI":"10.2514\/6.2005-6433"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing Higher Order Logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"3","key":"30_CR6","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.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf.\u00a07(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"30_CR7","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: Evaluating, testing, and animating PVS specifications. Technical report, Computer Science Laboratory. SRI International, Menlo Park, CA (March 2001)"},{"key":"30_CR8","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":"30_CR9","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit Paris Sud (March 2003)"},{"key":"30_CR10","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, number 364\/07 (August 2007)"},{"issue":"2","key":"30_CR11","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00165-006-0013-4","volume":"19","author":"B. Jacobs","year":"2007","unstructured":"Jacobs, B., Smetsers, S., Wichers Schreur, R.: Code-carrying theories. Formal Asp. Comput.\u00a019(2), 191\u2013203 (2007)","journal-title":"Formal Asp. Comput."},{"key":"30_CR12","unstructured":"Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall (1990)"},{"key":"30_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"30_CR14","unstructured":"Koser, J., Larsen, H., Vaughan, J.: SML2Java: a source to source translator. In: Proceedings of DP-Cool, PLI 2003, Uppsala,Sweden (2003)"},{"key":"30_CR15","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1109\/CSMR.2007.34","volume-title":"CSMR 2007: Proceedings of the 11th European Conference on Software Maintenance and Reengineering","author":"A.M. Leitao","year":"2007","unstructured":"Leitao, A.M.: Migration of Common Lisp programs to the Java platform -the Linj approach. In: CSMR 2007: Proceedings of the 11th European Conference on Software Maintenance and Reengineering, pp. 243\u2013251. IEEE Computer Society, Washington, DC (2007)"},{"key":"30_CR16","unstructured":"Lensink, L., Mu\u00f1oz, C.A., Goodloe, A.E.: From verified models to verifiable code. Technical Report NASA\/TM2009-215943, NASA Langley Research Center (2009)"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-30206-3_13","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"P. Miner","year":"2004","unstructured":"Miner, P., Geser, A., Pike, L., Maddalon, J.: A Unified Fault-Tolerance Protocol. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT 2004. LNCS, vol.\u00a03253, pp. 167\u2013182. Springer, Heidelberg (2004)"},{"key":"30_CR19","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Report NIA Report No. 2003-03, NASA\/CR-2003-212418, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA (May 2003)"},{"key":"30_CR20","unstructured":"Mu\u00f1oz, C., Goodloe, A.E.: Design and verification of a distributed communication protocol. Technical Report NASA\/CR-2009-215703 (2008)"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-Carrying Code. In: Proc. of POPL 1997, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"issue":"5\/6","key":"30_CR23","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. J. Symb. Comput.\u00a015(5\/6), 607\u2013640 (1993)","journal-title":"J. Symb. Comput."},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-30142-4_19","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Pike","year":"2004","unstructured":"Pike, L., Maddalon, J., Miner, P., Geser, A.: Abstractions for Fault-Tolerant Distributed System Verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 257\u2013270. Springer, Heidelberg (2004)"},{"key":"30_CR25","unstructured":"Ray, S.: Attaching Efficient Executability to Partial Functions in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX (November 2004)"},{"issue":"9","key":"30_CR26","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering\u00a024(9), 709\u2013720 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"30_CR27","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/32.210304","volume":"19","author":"J. Rushby","year":"1993","unstructured":"Rushby, J., von Henke, F.: Formal verification of algorithms for critical systems. IEEE Transactions on Software Engineering\u00a019(1), 13\u201323 (1993)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"30_CR28","unstructured":"Shankar, N.: Efficiently executing PVS. Technical report, Menlo Park, CA (1999)"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Static analysis for safe destructive updates in a functional language (2002)","DOI":"10.1007\/3-540-45607-4_1"},{"issue":"4","key":"30_CR30","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1017\/S0956796898003086","volume":"8","author":"A.P. Tolmach","year":"1998","unstructured":"Tolmach, A.P., Oliva, D.: From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming\u00a08(4), 367\u2013412 (1998)","journal-title":"Journal of Functional Programming"},{"key":"30_CR31","unstructured":"Urribarr\u00ed, W.: A module system for Why. Personal Communication (2008) manuscript"},{"key":"30_CR32","unstructured":"Wordsworth, J.: Software Development with Z. Addison-Wesley (1992)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T04:03:20Z","timestamp":1556510600000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}