{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:10:07Z","timestamp":1775052607950,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678984","type":"print"},{"value":"9783540446163","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/978-3-540-44616-3_1","type":"book-chapter","created":{"date-parts":[[2010,10,14]],"date-time":"2010-10-14T14:09:44Z","timestamp":1287065384000},"page":"1-21","source":"Crossref","is-referenced-by-count":14,"title":["A Type-Theoretic Memory Model for Verification of Sequential Java Programs"],"prefix":"10.1007","author":[{"given":"Joachim","family":"van den Berg","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"JavaCard API 2.1, \n                      http:\/\/java.sun.com\/products\/javacard\/htmldoc\/"},{"key":"1_CR2","volume-title":"The Java Programming Language","author":"K. Arnold","year":"1997","unstructured":"Arnold, K., Gosling, J.: The Java Programming Language, 2nd edn. Addison-Wesley, Reading (1997)","edition":"2"},{"key":"1_CR3","unstructured":"Bergstra, J., Loots, M.: Empirical semantics for object-oriented programs. Artificial Intelligence Preprint Series nr. 007, Dep. Philosophy, Utrecht Univ. (1999)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Borger, E., Schulte, W.: Initialization problems in Java. Software\u2014Concepts and Tools\u00a020(4) (1999)","DOI":"10.1007\/s003789900003"},{"key":"1_CR5","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"J.A. Goguen","year":"1996","unstructured":"Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)"},{"key":"1_CR6","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Griifioen","year":"1998","unstructured":"Griifioen, D., Huisman, M.: A comparison of PVS and Isabelle\/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 123\u2013142. Springer, Heidelberg (1998)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Huisman, M., Jacobs, B.: Inheritance in higher order logic: Modeling and reasoning. Techn. Rep. CSI-R0004, Comput. Sci. Inst., Univ. of Nijmegen (2000)","DOI":"10.1007\/3-540-44659-1_19"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"1_CR10","unstructured":"Huisman, M., Jacobs, B., van den Berg, J.: A case study in class library verification: Java\u2019s Vector class. Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. (An earlier version appeared in: Jacobs, B., Leavens, G.T., Miiller, P., Poetzsch-Heffter, A. (eds.), Formal Techniques for Java Programs. Proceedings of the ECOOP 1999 Workshop. Technical Report 251, Fernuniversitat Hagen (1999), pp. 37-44) (2000)"},{"key":"1_CR11","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-1-4613-1437-0_5","volume-title":"Object-Orientation with Parallelism and Persistence","author":"B. Jacobs","year":"1996","unstructured":"Jacobs, B.: Objects and classes, co-algebraically. In: Freitag, B., Jones, C.B., Lengauer, C., Schek, H.-J. (eds.) Object-Orientation with Parallelism and Persistence, pp. 83\u2013103. Kluwer Acad. Publ., Dordrecht (1996)"},{"key":"1_CR12","series-title":"Lecture Notes of Computer Science","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jacobs","year":"2000","unstructured":"Jacobs, B., Poll, E.: A monad forb asic Java semantics. In: Algebraic Methodology and Software Technology. Lecture Notes of Computer Science, Springer, Berlin (2000)"},{"key":"1_CR13","first-page":"222","volume":"62","author":"B. Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bulletin\u00a062, 222\u2013259 (1997)","journal-title":"EATCS Bulletin"},{"key":"1_CR14","first-page":"329","volume-title":"Object-Oriented Programming, Systems, Languages and Applications","author":"B. Jacobs","year":"1998","unstructured":"Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about classes in Java (preliminary report). In: Object-Oriented Programming, Systems, Languages and Applications, pp. 329\u2013340. ACM Press, New York (1998)"},{"key":"1_CR15","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Techn. Rep. 98-06, Dep. of Comp. Sci., Iowa State Univ. (1999), \n                      http:\/\/www.cs.iastate.edu\/leavens\/JML.html"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J.M., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. On Softw. Eng.\u00a021(2), 107\u2013125 (1995)","journal-title":"IEEE Trans. On Softw. Eng."},{"key":"1_CR17","series-title":"The APIC series","first-page":"361","volume-title":"Logic and computer science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and computer science. The APIC series, vol.\u00a031, pp. 361\u2013386. Academic Press, London (1990)"},{"key":"1_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., Miiller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) Programming Languages and Systems. LNCS, pp. 162\u2013176. Springer, Berlin (1999)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. Techn. Rep. CSI-R0005, Comput. Sci. Inst., Univ. of Nijmegen (2000)","DOI":"10.1007\/978-0-387-35528-3_8"},{"key":"1_CR20","unstructured":"Loop Project, \n                      http:\/\/www.cs.kun.nl\/~bart\/LOOP\/"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-44616-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:39:59Z","timestamp":1676691599000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-44616-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678984","9783540446163"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-44616-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}