{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:23Z","timestamp":1780994363672,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_23","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"266-280","source":"Crossref","is-referenced-by-count":18,"title":["Dynamic Logic with Non-rigid Functions"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030634","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, Springer, Heidelberg (1997)"},{"key":"23_CR2","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., 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\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe,, et al. (eds.) [4] (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","year":"2005","unstructured":"Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.): CASSIS 2004. LNCS, vol.\u00a03362. Springer, Heidelberg (2005)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B. Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, pp. 6\u201324. Springer, Heidelberg (2001)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36578-8_18","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Beckert","year":"2003","unstructured":"Beckert, B., Mostowski, W.: A program logic for handling Java Card\u2019s transaction mechanism. In: Pezz\u00e9, M. (ed.) ETAPS 2003 and FASE 2003. LNCS, vol.\u00a02621, Springer, Heidelberg (2003)"},{"key":"23_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/3-540-45744-5_51","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2001","unstructured":"Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 626\u2013641. Springer, Heidelberg (2001)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-24756-2_12","volume-title":"Integrated Formal Methods","author":"B. Beckert","year":"2004","unstructured":"Beckert, B., Schlager, S.: Software verification with integrated data type refinement for integer arithmetic. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 207\u2013226. Springer, Heidelberg (2004)"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe,, et al. (eds.) [4], pp. 108\u2013128 (2004)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"23_CR10","volume-title":"First-Order Modal Logic","author":"M. Fitting","year":"1999","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"23_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09237-4","volume-title":"First-Order Dynamic Logic","author":"D. Harel","year":"1979","unstructured":"Harel, D.: First-Order Dynamic Logic. Springer, New York (1979)"},{"issue":"3","key":"23_CR12","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/503502.503505","volume":"23","author":"A. Igarashi","year":"2001","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst.\u00a023(3), 396\u2013450 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) ETAPS 2001 and FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0053375","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"R. Miller","year":"1997","unstructured":"Miller, R., Tripathi, A.: Issues with exception handling in object-oriented systems. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 85\u2013103. Springer, Heidelberg (1997)"},{"key":"23_CR15","unstructured":"Mostowski, W.: Formal Development of Safe and Secure Java Card Applets. PhD thesis, Chalmers University of Technology, G\u00f6teborg, Sweden (February 2005)"},{"key":"23_CR16","unstructured":"Nipkow, T.: Jinja: Towards a comprehensive formal semantics for a Java-like language. In: Proc. Marktoberdorf Summer School (2003)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-39958-2_5","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"C. Pierik","year":"2003","unstructured":"Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 64\u201378. Springer, Heidelberg (2003)"},{"key":"23_CR18","unstructured":"Platzer, A.: An object-oriented dynamic logic with updates. Master\u2019s thesis, University of Karlsruhe (September 2004), available at www.key-project.org"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol.\u00a01576, Springer, Heidelberg (1999)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"St\u00e4rk, R., Nanchen, S.: A logic for abstract state machines. J. UCS\u00a07(11) (2001)","DOI":"10.1007\/3-540-44802-0_16"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-44616-3_1","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Berg van den","year":"2000","unstructured":"van den Berg, J., Huisman, M., Jacobs, B., Poll, E.: A type-theoretic memory model for verification of sequential Java programs. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 1\u201321. Springer, Heidelberg (2000)"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-45614-7_6","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 89\u2013105. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:33Z","timestamp":1605626073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11814771_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}