{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:50:34Z","timestamp":1725558634181},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203032"},{"type":"electronic","value":"9783540396567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_1","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:35:52Z","timestamp":1277836552000},"page":"1-32","source":"Crossref","is-referenced-by-count":9,"title":["A Tool-Supported Proof System for Multithreaded Java"],"prefix":"10.1007","author":[{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank S.","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem-Paul","family":"de Roever","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)"},{"key":"1_CR2","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: A Hoare logic for monitors in Java. Techical report TR-ST- 03-1, Lehrstuhl f\u00fcr Software-Technologie, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t zu Kiel (April 2003)"},{"key":"1_CR3","series-title":"LNCS State-of-the-Art-Survey","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS State-of-the-Art-Survey, vol.\u00a01523. Springer, Heidelberg (1999)"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K.R. Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.-P.: A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems\u00a02, 359\u2013385 (1980)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/BFb0030634","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Rustan, K., Leino, M.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 682\u2013696. Springer, Heidelberg (1997)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-44618-4_18","volume-title":"CONCUR 2000 - Concurrency Theory","author":"E. \u00c1brah\u00e1m-Mumm","year":"2000","unstructured":"\u00c1brah\u00e1m-Mumm, E., de Boer, F.S.: Proof-outlines for threads in Java. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, p. 229. Springer, Heidelberg (2000)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-45931-6_2","volume-title":"Foundations of Software Science and Computation Structures","author":"E. \u00c1brah\u00e1m-Mumm","year":"2002","unstructured":"\u00c1brah\u00e1m-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for Java\u2019s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 4\u201320. Springer, Heidelberg (2002); A longer version, including the proofs for soundness and completeness, appeared as Technical Report TR-ST-02-1 (March 2002)"},{"key":"1_CR8","unstructured":"America, P.: A behavioural approach to subtyping in objectoriented programming languages. 443, Phillips Research Laboratories (January\/April 1989)"},{"key":"1_CR9","volume-title":"Foundations of Multithreaded, Parallel, and Distributed Programming","author":"G.R. Andrews","year":"2000","unstructured":"Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Reading (2000)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods for Components and Objects","year":"2003","unstructured":"Bosangue, M., de Boer, F.S., de Roever, W.-P., Graf, S. (eds.): FMCO 2002. LNCS, vol.\u00a02852. Springer, Heidelberg (2003)"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214037.214100","volume":"27","author":"P.A. Buhr","year":"1995","unstructured":"Buhr, P.A., Fortier, M., Coffin, M.H.: Monitor classification. ACM Computing Surveys\u00a027(1), 63\u2013107 (1995)","journal-title":"ACM Computing Surveys"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-45685-6_5","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Basin","year":"2002","unstructured":"Basin, D., Friedrich, S., Gawkowski, M.: Verified bytecode model checkers. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 47\u201366. Springer, Heidelberg (2002)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: An event-based structural operational semantics of multi-threaded Java. In: Alves-Foss [AF99], pp. 157\u2013200","DOI":"10.1007\/3-540-48737-9_5"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-49019-1_10","volume-title":"Foundations of Software Science and Computation Structures","author":"F.S. Boer de","year":"1999","unstructured":"de Boer, F.S.: A WP-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 135\u2013156. Springer, Heidelberg (1999)"},{"key":"1_CR15","first-page":"163","volume-title":"Proceedings of the Fifth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002)","author":"F.S. Boer de","year":"2002","unstructured":"de Boer, F.S., Pierik, C.: Computer-aided specification and verification of annotated object-oriented programs. In: Jacobs, B., Rensink, A. (eds.) Proceedings of the Fifth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002), vol.\u00a0209, pp. 163\u2013177. Kluwer, Dordrecht (2002)"},{"key":"1_CR16","unstructured":"de Boer, F.S., Pierik, C.: Towards an environment for the verification of annotated object-oriented programs. Technical report UU-CS-2003-002, Institute of Information and Computing Sciences, University of Utrecht (January 2003)"},{"key":"1_CR17","unstructured":"de Figueiredo, C.C.: A proof system for a sequential object-oriented language. Technical Report UMCS-95-1-1, University of Manchester (1995)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proc. Symp. in Applied Mathematics, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"1_CR19","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_CR20","series-title":"International Series in Computer Science","volume-title":"Essays in Computing Science","year":"1989","unstructured":"Hoare, C.A.R., Jones, C.B. (eds.): Essays in Computing Science. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012, 576\u2013580 (1969); Also in [HJ89]","journal-title":"Communications of the ACM"},{"key":"1_CR22","unstructured":"Huisman, M.: Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen (2001)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: Bosangue et al. [BdBdRG03]","DOI":"10.1007\/978-3-540-39656-7_8"},{"key":"1_CR24","first-page":"329","volume-title":"Object Oriented Programing: Systems, Languages, and Applications (OOPSLA) 1998","author":"B. Jacobs","year":"1998","unstructured":"Jacobs, B., van den Berg, J., Huisman, M., van Barkum, M., Hensel, U., Tews, H.: Reasoning about classes in Java (preliminary report). In: Object Oriented Programing: Systems, Languages, and Applications (OOPSLA) 1998, pp. 329\u2013340. ACM, New York (1998) (in SIGPLAN Notices)"},{"key":"1_CR25","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modelling language. In: Formal Underpinnings of Java Workshop, at OOPSLA 1998 (1998)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of jml accommodates both runtime assertion checking and formal verification. In: Bosangue, et al. [BdBdRG03]","DOI":"10.1007\/978-3-540-39656-7_11"},{"issue":"3","key":"1_CR27","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BF00289266","volume":"15","author":"G.M. Levin","year":"1981","unstructured":"Levin, G.M., Gries, D.: A proof technique for communicating sequential processes. Acta Informatica\u00a015(3), 281\u2013302 (1981)","journal-title":"Acta Informatica"},{"key":"1_CR28","unstructured":"The LOOP project: Formal methods for object-oriented systems (2001), http:\/\/www.cs.kun.nl\/~bart\/LOOP\/"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1145\/97945.97970","volume-title":"Object Oriented Programing: Systems, Languages, and Applications (OOPSLA) 1990","author":"G.T. Leavens","year":"1990","unstructured":"Leavens, G.T., Wheil, W.E.: Reasoning about objectoriented programs that use subtypes. In: Object Oriented Programing: Systems, Languages, and Applications (OOPSLA) 1990, Ottawa, Canada, pp. 212\u2013223. ACM, New York (1990); Extended Abstract"},{"key":"#cr-split#-1_CR30.1","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Wheil, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica (1994);","DOI":"10.1007\/s002360050032"},{"key":"#cr-split#-1_CR30.2","unstructured":"An expanded version appeared as Iowa State Unversity Report, 92-28d"},{"issue":"4","key":"1_CR31","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica\u00a06(4), 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. Technical report UU-CS-2003- 010, Institute of Information and Computing Sciences, University of Utrecht (2003)","DOI":"10.1007\/978-3-540-39958-2_5"},{"key":"1_CR34","unstructured":"Poetzsch-Heffter, A.: A logic for the verification of object-oriented programs. In: Berghammer, R., Simon, F. (eds.) Proceedings of Programming Languages and Fundamentals of Programming, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, November 1997. Bericht Nr. 9717, pp. 31\u201342 (1997)"},{"key":"1_CR35","unstructured":"Poetzsch-Heffter, A.: Specification and Verification of Object- Oriented Programs. Technische Universit\u00e4t M\u00fcnchen, Habilitationsschrift (January 1997)"},{"key":"1_CR36","series-title":"International Federation for Information Processing (IFIP)","volume-title":"Proceedings of PROCOMET 1998","author":"A. Poetzsch-Heffter","year":"1998","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: Logical foundations for typed object-oriented languages. In: Gries, D., de Roever, W.-P. (eds.) Proceedings of PROCOMET 1998. International Federation for Information Processing (IFIP). Chapman & Hall, Boca Raton (1998)"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","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., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-45314-8_22","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Reus","year":"2001","unstructured":"Reus, B., Hennicker, R., Wirsing, M.: A Hoare calculus for verifying Java realizations of OCL-constrained design models. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 300\u2013316. Springer, Heidelberg (2001)"},{"key":"1_CR39","unstructured":"Reus, B., Wirsing, M.: A Hoare-logic for object-oriented programs. Technical report, LMU M\u00fcnchen (2000)"},{"key":"1_CR40","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer, Heidelberg (2001)"},{"key":"#cr-split#-1_CR41.1","unstructured":"Tang, F., Hofmann, M.: Generation of verification conditions for Abadi and Leino???s logic of objects (extended abstract). In: Proceedings of the 9th International Workshop on Foundations of Object- Oriented Languages, FOOL 2002 (2002);"},{"key":"#cr-split#-1_CR41.2","unstructured":"A longer version is available as LFCS technical report"},{"issue":"13","key":"1_CR42","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D. Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurrency and Computation: Practice and Experience\u00a013(13), 1173\u20131214 (2001)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"1_CR43","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)"},{"key":"1_CR44","series-title":"Object Technology Series","volume-title":"The Object Constraint Language: Precise Modeling With Uml","author":"J.B. Warmer","year":"1999","unstructured":"Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Precise Modeling With Uml. Object Technology Series. Addison-Wesley, Reading (1999)"}],"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-540-39656-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T14:57:13Z","timestamp":1559228233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}