{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:47Z","timestamp":1725490247848},"publisher-location":"Berlin, Heidelberg","reference-count":64,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540669548"},{"type":"electronic","value":"9783540465898"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46589-8_6","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T15:05:53Z","timestamp":1188313553000},"page":"97-115","source":"Crossref","is-referenced-by-count":6,"title":["Formal Techniques for Java Programs"],"prefix":"10.1007","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,4,12]]},"reference":[{"key":"6_CR1","isbn-type":"print","volume-title":"Monographs in Computer Science","author":"M. Abadi","year":"1996","unstructured":"M. Abadi and L. Cardelli. A Theory of Objects. Monographs in Computer Science. Springer-Verlag, New York, 1996. ISBN 0-387-94775-2.","ISBN":"http:\/\/id.crossref.org\/isbn\/0387947752"},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/BFb0030634","volume-title":"Proc. TAPSOFT\u2019 97, 7th Int. Joint Conference CAAP\/FASE","author":"M. Abadi","year":"1997","unstructured":"M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In M. Bidoit and M. Dauchet, (eds.): Proc. TAPSOFT\u2019 97, 7th Int. Joint Conference CAAP\/FASE, vol. 1214, LNCS, pp. 682\u2013696. Springer, 1997."},{"key":"6_CR3","unstructured":"A. Aiken and N. Heintze, Constraint-based program analysis. Tutorial of 22th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Januaray 1995."},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/258077.258078","volume":"6","author":"R. Allen","year":"1997","unstructured":"R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, 6(3):213\u2013249, June 1997.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"J. Alves-Foss, (ed.): Formal Syntax and Semantics of Java. LNCS, vol. 1523, Springer, 1999."},{"key":"6_CR6","unstructured":"K. Arnold and J. Gosling. The Java Programming Language. Addison-Wesley, 2nd edition, 1997."},{"key":"6_CR7","unstructured":"D. Bartetzko. Parallelit\u00e4t und Vererbung beim \u2018Programmieren mit Vertrag\u2019. Master\u2019s thesis, University of Oldenburg, May 1999. in German."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"J. Bicarregui, K. Lano, and T. Maibaum: Towards a Compositional Interpretation of Object Diagrams. Technical Report, Department of Computing, Imperial College, 1997.","DOI":"10.1007\/978-0-387-35264-0_8"},{"key":"6_CR9","unstructured":"E. B\u00f6rger and W. Schulte. A programmer friendly modular definition of the semantics of Java. http:\/\/www.informatik.uni-ulm.de\/pm\/mitarbeiter\/wolfram.html ."},{"key":"6_CR10","unstructured":"P. Cenciarelli. Computational applications of calculi based on monads. PhD thesis, Department of Computer Science, University of Edinburgh, 1995. CST-127-96._Also available as ECS-LFCS-96-346."},{"key":"6_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of 7th International Conference on Algebraic Methodology and Software Technology (AMAST\u201998)","author":"P. Cenciarelli","year":"1998","unstructured":"P. Cenciarelli. An Algebraic View of Program Composition. In Armando Haeberer, editor, Proceedings of 7th International Conference on Algebraic Methodology and Software Technology (AMAST\u201998), 1998. LNCS 1548."},{"key":"6_CR12","unstructured":"P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of 5th Biennial Meeting on Category Theory and Computer Science. CTCS-5, 1993. CWI Tech. Report."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. From sequential to multithreaded Java: an event-based operational semantics. In 6th Conf. Algebraic Methodology and Software Technology, AMAST, 1997.","DOI":"10.1007\/BFb0000464"},{"key":"6_CR14","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 [5].","DOI":"10.1007\/3-540-48737-9_5"},{"key":"6_CR15","unstructured":"S. Cimato. A Methodology for the Specification and Verification of Java Components and Architectures. PhD thesis, Dept. of Computer Science, University of Bologna, Italy, February 1999."},{"key":"6_CR16","unstructured":"A.N. Clark and A.S. Evans: Semantic Foundations of the Unified Modelling Language. In the proceedings of the First Workshop on Rigorous Object-Oriented Methods: ROOM 1, Imperial College, June, 1997."},{"key":"6_CR17","unstructured":"A.N. Clark: A Semantics for Object-Oriented Systems. Presented at the Third Northern Formal Methods Workshop. September 1998. In BCS FACS Electronic Workshops in Computing, 1999."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"A.N. Clark: A Semantics for Object-Oriented Design Notations. Technical report, submitted to the BCS FACS Journal, 1999.","DOI":"10.14236\/ewic\/NFM1998.5"},{"key":"6_CR19","unstructured":"R. Cohen. Defensive Java Virtual Machine Specification. http:\/\/www.cli.com\/software\/djvm ."},{"key":"6_CR20","unstructured":"E. Coscia and G. Reggio. An operational semantics for java. Departimento di Informatica e Scienze dell\u2019 Informazione, Universita di Genova, http:\/\/www.disi.unige.it ."},{"key":"6_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49019-1_10","volume-title":"Foundations of Software Sci. and Comp. Struct.","author":"F.S. Boer de","year":"1999","unstructured":"F.S. de Boer. A wp-calculus for OO. In W. Thomas, (ed.), Foundations of Software Sci. and Comp. Struct., vol. 1578 of LNCS. Springer, 1999."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"G. DeFouw, D. Grove, and C. Chambers, Fast interprocedural class analysis, Proceedings of 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages pages 222\u2013236, Januaray 1998.","DOI":"10.1145\/268946.268965"},{"key":"6_CR23","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976."},{"key":"6_CR24","unstructured":"S. Drossopoulou and S. Eisenbach. Is the Java type system sound? In Fourth International Workshop on Foundations of Object-Oriented Languages, October 1997. http:\/\/www.outoften.doc.ic.ac.uk\/projects\/slurp\/papers.html ."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In 11th European Conference on Object-Oriented Programming, February 1997. http:\/\/www.outoften.doc.ic.ac.uk\/projects\/slurp\/papers.html .","DOI":"10.1007\/BFb0053388"},{"key":"6_CR26","unstructured":"S. Drossopoulou and S. Eisenbach. Towards an operational semantics and proof of type soundness for java, April 1998. http:\/\/www.outoften.doc.ic.ac.uk\/projects\/slurp\/papers.html ."},{"key":"6_CR27","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/0920-5489(95)00024-O","volume":"17","author":"R. Duke","year":"1995","unstructured":"R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511\u2013533, 1995.","journal-title":"Computer Standards and Interfaces"},{"key":"6_CR28","unstructured":"Extended Static Checking home page, Compaq Systems Research Center. On the Web at http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html ."},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS\u2019 97), volume 2, pages 423\u2013438. Chapman & Hall, 1997.","DOI":"10.1007\/978-0-387-35261-9_29"},{"issue":"4","key":"6_CR30","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1080\/03081077408960783","volume":"1","author":"J. Goguen","year":"1975","unstructured":"J. Goguen: Objects. Int. Journal of General Systems, 1(4):237\u2013243, 1975.","journal-title":"Int. Journal of General Systems"},{"key":"6_CR31","unstructured":"J. Goguen: Sheaf Semantics for Concurrent Interacting Objects. Mathematical Structures in Computer Science, 1990."},{"key":"6_CR32","unstructured":"A. Gontmakher and A. Schuster. Java consistency: Non-operational characterizations for java memory behaviour. Technical Report CS0922, Computer Science Department, Technion, November 1997."},{"key":"6_CR33","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"6_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J. Guttag","year":"1993","unstructured":"J. Guttag and J. Horning. Larch: Languages and Tools for Formal Specification. Springer-Verlag, Berlin, 1993."},{"key":"6_CR35","unstructured":"N. Heintze, Set-based program analysis. Ph.D thesis, Carnegie Mellon University, October 1992."},{"issue":"1","key":"6_CR36","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1006\/inco.1996.0031","volume":"126","author":"M. Hofmann","year":"1996","unstructured":"M. Hofmann and B. Pierce. Positive subtyping. Information and Computation, 126(1):186\u2013197, 1996.","journal-title":"Information and Computation"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"B. Jacobs. Coalgebraic reasoning about classes in object-oriented languages. In CMCS 1998, number 11 in Electr. Notes in Comp. Sci. Elsevier, 1998.","DOI":"10.1016\/S1571-0661(04)00061-1"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about classes in Java (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329\u2013340. ACM Press, 1998.","DOI":"10.1145\/286942.286973"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"B. Jacobs, G.T. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter, editors. Formal Techniques for Java Programs. Technical Report 251, Fernuniversit\u00e4t Hagen, 1999. URL: http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html .","DOI":"10.1007\/3-540-46589-8_6"},{"key":"6_CR40","unstructured":"Jass: Java with assertions, May 1999. http:\/\/www.semantik.informatik.uni-oldenburg.de\/~jass ."},{"key":"6_CR41","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CONCUR\u201993","author":"C. Jones","year":"1993","unstructured":"C. Jones. A pi-calculus semantics for an object-based design notation. In Proc. of CONCUR\u201993, 1993. LNCS 715."},{"issue":"4","key":"6_CR42","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/52.300040","volume":"8","author":"G.T. Leavens","year":"1991","unstructured":"G.T. Leavens. Modular specification and verification of object-oriented programs. IEEE Software, 8(4):72\u201380, 1991.","journal-title":"IEEE Software"},{"key":"6_CR43","unstructured":"K.R.M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. Tech. Report KRML 65-0, SRC, 1996."},{"issue":"4","key":"6_CR44","first-page":"330","volume":"5","author":"K.R.M. Leino","year":"1998","unstructured":"K.R.M. Leino. Recursive object types in a logic of object-oriented programs. Nordic Journal of Computing, 5(4):330\u2013360, 1998.","journal-title":"Nordic Journal of Computing"},{"key":"6_CR45","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-60406-5_12","volume-title":"Proc. 5th European Software Engineering Conf. (ESEC 95)","author":"J. Magee","year":"1995","unstructured":"J. Magee, N. Dulay, S. Eisenbach, and J. Kramer. Specifying Distributed Software Architectures. In Proc. 5th European Software Engineering Conf. (ESEC 95), v. 989 of LNCS, pp. 137\u2013153, Sitges, Spain, September 1995."},{"key":"6_CR46","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall, 1988."},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"R. Milner. Implementation and application of Scott\u2019s logic of continuous functions. In Conf. on Proving Assertions About Programs, pp. 1\u20136. SIGPLAN 1, 1972.","DOI":"10.1145\/800235.807067"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"6_CR49","unstructured":"E. Moggi. An abstract view of programming languages. Technical Report ECSLFCS-90-113, University of Edinburgh, Comp. Sci. Dept., 1990."},{"key":"6_CR50","doi-asserted-by":"crossref","unstructured":"E. Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"6_CR51","unstructured":"T. Nipkow and D. von Oheimb. Machine-checking the Java Specification: Proving Type-Saftey. In [5]."},{"key":"6_CR52","doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. von Oheimb. Javalight is Type-Safe-Definitely. 25th ACM symposium on Principles of Programming Languages, 1998.","DOI":"10.1145\/268946.268960"},{"key":"6_CR53","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification (CAV\u2019 96)","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer-Aided Verification (CAV\u2019 96), volume 1102 of LNCS, pages 411\u2013414, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"6_CR54","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TPPP\u201994","author":"B. Pierce","year":"1995","unstructured":"B. Pierce and D. Turner. Concurrent objects in a process calculus. In Proceedings of TPPP\u201994. Springer LNCS 907, 1995."},{"key":"6_CR55","unstructured":"A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Technical report, Technical University of Munich, 1997. Habilitation Thesis."},{"key":"6_CR56","doi-asserted-by":"crossref","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S.D. Swierstra, editor, Programming Languages and Systems (ESOP\u2019 99), volume 1576, pages 162\u2013176. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-49099-X_11"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"W. Pugh. Fixing the java memory model. In Java Grande, June 1999.","DOI":"10.1145\/304065.304106"},{"key":"6_CR58","unstructured":"Z. Qian. Least Types for Memory Locations in Java Bytecode. Kestrel Institute, Tech Report, 1998."},{"key":"6_CR59","unstructured":"A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997."},{"key":"6_CR60","doi-asserted-by":"crossref","unstructured":"A. Ruiz-Delgado, D. Pitt, and C. Smythe: A Review of Object-Oriented Approaches in Formal Specification. The Computer Journal, 38(10), 1995.","DOI":"10.1093\/comjnl\/38.10.777"},{"key":"6_CR61","unstructured":"D. Syme. Proving Java Type Soundness. Technical report, University of Cambridge Computer Laboratory, 1997."},{"issue":"1","key":"6_CR62","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"J. Wing","year":"1987","unstructured":"J. Wing. Writing Larch Interface Language Specifications. ACM Transactions on Programming Languages and Systems, 9(1):1\u201324, January 1987.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR63","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/BFb0032736","volume-title":"proceedings of the 4th international static analysis symposium edition","author":"K. Yi","year":"1997","unstructured":"K. Yi and S. Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Lecture Notes in Computer Science, volume 1302, pages 98\u2013113. Springer-Verlag, proceedings of the 4th international static analysis symposium edition, 1997."},{"key":"6_CR64","doi-asserted-by":"crossref","unstructured":"K. Yi and S. Ryu. SML\/NJ Exception Analysis version 0.98. http:\/\/www.compiler.kaist.ac.kr\/pub\/exna\/ , December 1998.","DOI":"10.1007\/BFb0032736"}],"container-title":["Lecture Notes in Computer Science","Object-Oriented Technology ECOOP\u201999 Workshop Reader"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46589-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,26]],"date-time":"2020-04-26T05:14:57Z","timestamp":1587878097000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46589-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540669548","9783540465898"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/3-540-46589-8_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}