{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:37:07Z","timestamp":1725896227662},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_20","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"283-295","source":"Crossref","is-referenced-by-count":3,"title":["PE-KeY: A Partial Evaluator for Java Programs"],"prefix":"10.1007","author":[{"given":"Ran","family":"Ji","sequence":"first","affiliation":[]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"LNAI","first-page":"410","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334, pp. 410\u2013451. Springer, Heidelberg (2007)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-25271-6_5","volume-title":"Formal Methods for Components and Objects","author":"R. Bubel","year":"2011","unstructured":"Bubel, R., H\u00e4hnle, R., Ji, R.: Program Specialization via a Software Verification Tool. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 80\u2013101. Springer, Heidelberg (2011)"},{"key":"20_CR3","unstructured":"King, J.C.: A program verifier. PhD thesis, CMU (1969)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-17071-3_7","volume-title":"Formal Methods for Components and Objects","author":"R. Bubel","year":"2010","unstructured":"Bubel, R., H\u00e4hnle, R., Ji, R.: Interleaving Symbolic Execution and Partial Evaluation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 125\u2013146. Springer, Heidelberg (2010)"},{"issue":"4","key":"20_CR5","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1145\/778559.778561","volume":"25","author":"U.P. Schultz","year":"2003","unstructured":"Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for Java. ACM-TPLS\u00a025(4), 452\u2013499 (2003)","journal-title":"ACM-TPLS"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Shali, A., Cook, W.R.: Hybrid partial evaluation. In: OOPSLA, pp. 375\u2013390 (2011)","DOI":"10.1145\/2076021.2048098"},{"key":"20_CR7","unstructured":"Ruf, E.S.: Topics in online partial evaluation. PhD thesis, Stanford University, Stanford, CA, USA, UMI Order No. GAX93-26550 (1993)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BFb0026826","volume-title":"Programming Languages: Implementations, Logics and Programs","author":"J. Hatcliff","year":"1995","unstructured":"Hatcliff, J.: Mechanically Verifying the Correctness of an Offline Partial Evaluator. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol.\u00a0982, pp. 279\u2013298. Springer, Heidelberg (1995)"},{"issue":"5","key":"20_CR9","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1017\/S0960129597002405","volume":"7","author":"J. Hatcliff","year":"1997","unstructured":"Hatcliff, J., Danvy, O.: A computational formalization for partial evaluation. Mathematical Structures in Computer Science\u00a07(5), 507\u2013541 (1997)","journal-title":"Mathematical Structures in Computer Science"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050, 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes\u00a028, 2 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1145\/800055.802038","volume-title":"Proc. of the ACM Symposium LFP 1984","author":"L. Augustsson","year":"1984","unstructured":"Augustsson, L.: A compiler for lazy ML. In: Proc. of the ACM Symposium LFP 1984, pp. 218\u2013227. ACM, New York (1984)"},{"key":"20_CR13","unstructured":"Breebaart, L.: Rule-based compilation of data parallel programs. PhD thesis, Delft University of Technology (2003)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/11513988_29","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2005","unstructured":"Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.D.: TVOC: A Translation Validator for Optimizing Compilers. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 291\u2013295. Springer, Heidelberg (2005)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer (2001)","DOI":"10.1007\/978-3-642-59495-3"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21455-4_13","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"D. Clarke","year":"2011","unstructured":"Clarke, D., Diakov, N., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I., Sch\u00e4fer, J., Schlatte, R., Wong, P.Y.H.: Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 417\u2013457. Springer, Heidelberg (2011)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-25271-6_11","volume-title":"Formal Methods for Components and Objects","author":"D. Clarke","year":"2011","unstructured":"Clarke, D., Muschevici, R., Proen\u00e7a, J., Schaefer, I., Schlatte, R.: Variability Modelling in the ABS Language. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 204\u2013224. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:28:56Z","timestamp":1620127736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}