{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:01:57Z","timestamp":1743012117571,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642170706"},{"type":"electronic","value":"9783642170713"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17071-3_7","type":"book-chapter","created":{"date-parts":[[2010,11,11]],"date-time":"2010-11-11T07:12:58Z","timestamp":1289459578000},"page":"125-146","source":"Crossref","is-referenced-by-count":6,"title":["Interleaving Symbolic Execution and Partial Evaluation"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bubel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ran","family":"Ji","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)","key":"7_CR1"},{"key":"7_CR2","volume-title":"Partial evaluation and automatic program generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"7_CR3","series-title":"LNCS","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2006","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol.\u00a04334. Springer, Heidelberg (2006)"},{"key":"7_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11814771_23","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2006","unstructured":"Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 266\u2013280. Springer, Heidelberg (2006)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Specification and Design of Software Systems","author":"M. Heisel","year":"1985","unstructured":"Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Knuth, E., Neuhold, E.J. (eds.) Operating Systems 1982. LNCS, vol.\u00a0152, Springer, Heidelberg (1985)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-24732-6_13","volume-title":"Model Checking Software","author":"C.S. Pasareanu","year":"2004","unstructured":"Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 164\u2013181. Springer, Heidelberg (2004)"},{"key":"7_CR7","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.M., 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)"},{"unstructured":"Baum, M.: Debugging by visualizing of symbolic execution. Master\u2019s thesis, Dept.of Computer Science, Institute for Theoretical Computer Science (June 2007)","key":"7_CR8"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-79124-9_12","volume-title":"Tests and Proofs","author":"J. Halleux de","year":"2008","unstructured":"de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 171\u2013181. Springer, Heidelberg (2008)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73770-4_10","volume-title":"Tests and Proofs","author":"C. Engel","year":"2007","unstructured":"Engel, C., H\u00e4hnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 169\u2013188. Springer, Heidelberg (2007)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"},{"key":"7_CR12","first-page":"157","volume-title":"Proc. 21st IEEE\/ASM Intl. Conference on Automated Software Engineering","author":"X. Deng","year":"2006","unstructured":"Deng, X., Lee, J.: Robby: Bogor\/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: Proc. 21st IEEE\/ASM Intl. Conference on Automated Software Engineering, Tokyo, Japan, pp. 157\u2013166. IEEE Computer Society, Los Alamitos (2006)"},{"unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (August 2008)","key":"7_CR13"},{"doi-asserted-by":"crossref","unstructured":"Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for java. ACM Transactions on Programming Languages and Systems\u00a025 (2003)","key":"7_CR14","DOI":"10.1145\/778559.778561"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-04167-9_13","volume-title":"Formal Methods for Components and Objects","author":"R. Bubel","year":"2009","unstructured":"Bubel, R., H\u00e4hnle, R., Weiss, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol.\u00a05751, pp. 247\u2013277. Springer, Heidelberg (2009)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-00255-7_10","volume-title":"Integrated Formal Methods","author":"B. Wei\u00df","year":"2009","unstructured":"Wei\u00df, B.: Predicate abstraction in a program logic calculus. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 136\u2013150. Springer, Heidelberg (2009)"},{"unstructured":"Engel, C., Roth, A., Schmitt, P.H., Wei\u00df, B.: Verification of modifies clauses in dynamic logic with non-rigid functions. Technical Report 2009-9, Department of Computer Science, University of Karlsruhe (2009)","key":"7_CR17"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF03038271","volume":"12","author":"D. Sahlin","year":"1993","unstructured":"Sahlin, D.: Mixtus: an automatic partial evaluator for full prolog. New Gen. Comput.\u00a012(1), 7\u201351 (1993)","journal-title":"New Gen. Comput."},{"doi-asserted-by":"crossref","unstructured":"Glenstrup, A.J., Makholm, H., Secher, J.P.: C-mix: Specialization of c programs. Partial Evaluation, 108\u2013154 (1998)","key":"7_CR19","DOI":"10.1007\/3-540-47018-2_4"},{"issue":"3","key":"7_CR20","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"V.F. Turchin","year":"1986","unstructured":"Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst.\u00a08(3), 292\u2013325 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR21","volume-title":"ACM SIGPLAN WS on Partial Evaluation and Semantics-based Program Manipulation","author":"E. Albert","year":"2010","unstructured":"Albert, E., Gomez-Zamalloa, M., Puebla, G.: PET: a partial evaluation-based test case generation tool for Java bytecode. In: ACM SIGPLAN WS on Partial Evaluation and Semantics-based Program Manipulation. ACM Press, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17071-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T01:56:53Z","timestamp":1559786213000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17071-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642170706","9783642170713"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17071-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}