{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T08:43:42Z","timestamp":1743497022530},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433668"},{"type":"electronic","value":"9783540459316"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45931-6_2","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:53:52Z","timestamp":1181350432000},"page":"5-20","source":"Crossref","is-referenced-by-count":21,"title":["Verification for Java\u2019s Reentrant Multithreading Concept"],"prefix":"10.1007","author":[{"given":"Erika","family":"\u00c1brah\u00e1m-Mumm","sequence":"first","affiliation":[]},{"given":"Frank S.","family":"de Boer","sequence":"additional","affiliation":[]},{"given":"Willem-Paul","family":"de Roever","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,3,15]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Bidoit and Dauchet [9], pages 682\u2013696.","DOI":"10.1007\/BFb0030634"},{"key":"2_CR2","unstructured":"E. \u00c1brah\u00e1m-Mumm and F. de Boer. Proof-outlines for threads in Java. In Palamidessi [25]."},{"key":"2_CR3","unstructured":"E. \u00c1brah\u00e1m-Mumm, F. de Boer, W.-P. de Roever, and M. Steffen. Verification for Java\u2019s reentrant multithreadingconcept: Soundness and completeness. Technical Report TR-ST-01-2, Lehrstuhl f\u00fcr Software-Technologie, Institut f\u00fcr Informatik und praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, 2001."},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"J. Alves-Foss, editor. Formal Syntax and Semantics of Java. LNCS State-of-the-Art-Survey. Springer, 1999."},{"key":"2_CR5","unstructured":"P. America. A behavioural approach to subtypingin object-oriented programming languages. Technical report 443, Phillips Research Laboratories, 1989."},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01215408","volume":"6","author":"P. America","year":"1993","unstructured":"P. America and F. Boer. Reasoningab out dynamically evolvingpro cess structures. Formal Aspects of Computing, 6(3):269\u2013316, 1993.","journal-title":"Formal Aspects of Computing"},{"issue":"4","key":"2_CR7","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"K. R. Apt. Ten years of Hoare\u2019s logic: A survey-part I. ACM Transact. on Progr. Lang. and Syst., 3(4):431\u2013483, 1981.","journal-title":"ACM Transact. on Progr. Lang. and Syst."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K. R. Apt","year":"1980","unstructured":"K. R. Apt, N. Francez, and W.-P. de Roever. A proof system for communicating sequential processes. ACM Transact. on Progr. Lang. and Syst., 2:359\u2013385, 1980.","journal-title":"ACM Transact. on Progr. Lang. and Syst."},{"key":"2_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Theory and Practice of Software Development","year":"1997","unstructured":"M. Bidoit and M. Dauchet, editors. Theory and Practice of Software Development, Proc. of the 7th Int. Joint Conf. of CAAP\/FASE, TAPSOFT\u201997, volume 1214 of LNCS. Springer, 1997."},{"key":"2_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-54972-2","volume-title":"Algebraic Specification Techniques in Object Oriented Programming Environments","author":"R. Breu","year":"1991","unstructured":"R. Breu. Algebraic Specification Techniques in Object Oriented Programming Environments. PhD thesis, Universit\u00e4t Passau, 1991. See also Springer LNCS 562."},{"issue":"1","key":"2_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214037.214100","volume":"27","author":"P. A. Buhr","year":"1995","unstructured":"P. A. Buhr, M. Fortier, and M. H. Coffin. Monitor classification. ACM Computing Surveys, 27(1):63\u2013107, 1995.","journal-title":"ACM Computing Surveys"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An event-based structural operational semantics of multi-threaded Java. In Alves-Foss [4].","DOI":"10.1007\/3-540-48737-9_5"},{"key":"2_CR13","unstructured":"W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, 2001."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Proc. Sym. in Applied Mathematics, volume 19, pages 19\u201332, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"2_CR15","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"2_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Programming Languages and Systems","year":"1998","unstructured":"C. Hankin, editor. Programming Languages and Systems: Proc. of ESOP\u2019 98, Held as Part of ETAPS\u2019 98, volume 1381 of LNCS. Springer, 1998."},{"key":"2_CR17","unstructured":"J. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoningab out classes in objectoriented languages: Logical models and tools. In Hankin [16]."},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576\u2013580, 1969. Also in [19].","journal-title":"Communications of the ACM"},{"key":"2_CR19","unstructured":"C. A. R. Hoare and C. B. Jones, editors. Essays in Computing Science. International Series in Computer Science. Prentice Hall, 1989."},{"key":"2_CR20","unstructured":"M. Huisman. Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001."},{"key":"2_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Fundamental Approaches to Software Engineering","year":"2001","unstructured":"H. Hussmann, editor. Fundamental Approaches to Software Engineering, volume 2029 of LNCS. Springer, 2001."},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BF00289266","volume":"15","author":"G. M. Levin","year":"1981","unstructured":"G. M. Levin and D. Gries. A proof technique for communicating sequential processes. Acta Informatica, 15(3):281\u2013302, 1981.","journal-title":"Acta Informatica"},{"key":"2_CR23","unstructured":"The LOOP project: Formal methods for object-oriented systems. http:\/\/www.cs.kun.nl\/~bart\/LOOP\/ , 2001."},{"issue":"4","key":"2_CR24","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"2_CR25","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR 2000","year":"2000","unstructured":"C. Palamidessi, editor. CONCUR 2000, volume 1877 of LNCS. Springer, 2000."},{"key":"2_CR26","unstructured":"A. Poetzsch-Heffter. Specification and Verification of Object-Oriented Programs. Technische Universit\u00e4t M\u00fcnchen, 1997. Habilitationsschrift."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In Swierstra [30], pages 162\u2013176.","DOI":"10.1007\/3-540-49099-X_11"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"B. Reus, R. Hennicker, and M. Wirsing. A Hoare calculus for verifying Java realizations of OCL-constrained design models. In Hussmann [21], pages 300\u2013316.","DOI":"10.1007\/3-540-45314-8_22"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"R. St\u00e4rk, J. Schmid, and E. B\u00f6rger. Java and the Java Virtual Machine. Springer, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"2_CR30","series-title":"Lect Notes Comput Sci","volume-title":"Proc.of ESOP\u2019 99","year":"1999","unstructured":"S. Swierstra, editor. Proc.of ESOP\u2019 99, volume 1576 of LNCS. Springer, 1999."},{"key":"2_CR31","unstructured":"D. von Oheimb. Axiomatic sematics for Javalight in Isabelle\/HOL. In S. Drossopoulo, S. Eisenbach, B. Jacobs, G. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs, number 269, 5\/2000 in Technical Report. Fernuniversit\u00e4t Hagen, 2000."},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"D. von Oheimb. Hoare logic for Java in Isabelle\/HOL. Concurrency-Practice and Experience, 2001. To appear.","DOI":"10.1002\/cpe.598"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"D. von Oheimb and T. Nipkow. Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. Submitted for publication, 2002.","DOI":"10.1007\/3-540-45614-7_6"},{"key":"2_CR34","unstructured":"J. B. Warmer and A. G. Kleppe. The Object Constraint Language: Precise Modeling With Uml. Object Technology Series. Addison-Wesley, 1999."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45931-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:19:28Z","timestamp":1556479168000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45931-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433668","9783540459316"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45931-6_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}