{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:11:03Z","timestamp":1737349863014,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540436751"},{"type":"electronic","value":"9783540478539"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47853-1_3","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T18:12:38Z","timestamp":1186423958000},"page":"30-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Techniques for Java Programs"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophia","family":"Drossopoulou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"3_CR1","unstructured":"D. Ancona, G. Lagorio, and E. Zucca. Java separate type checking is not safe. Available in [DEL+01], 2001."},{"key":"3_CR2","unstructured":"P. Boury and N. Elkhadi. Static analysis of Java cryptographic applets. Available in [DEL+01], 2001."},{"key":"3_CR3","unstructured":"G. Barthe, D. Gurov, and M. Huisman. Compositional specification and verification of control flow based security properties of multi-application programs. Available in [DEL+01], 2001."},{"key":"3_CR4","unstructured":"J. Boyland. The interdependence of effects and uniqueness. Available in [DEL+01], 2001."},{"key":"3_CR5","unstructured":"M. Carbone, M. Coccia, G. Ferrari, and S. Maffeis. Process algebra-guided design of Java mobile network applications. Available in [DEL+01], 2001."},{"key":"3_CR6","unstructured":"A. Cavalcanti and D. Naumann. Class refinement for sequential Java. Available in [DEL+01], 2001."},{"key":"3_CR7","unstructured":"A. Coglio. Improving the official specification of Java bytecode verification. Available in [DEL+01], 2001."},{"key":"3_CR8","volume-title":"Technical report","author":"A. Coglio","year":"2001","unstructured":"A. Coglio. Java bytecode verification: A complete formalization. Technical report, Kestrel Institute, Palo Alto, 2001. Forthcoming at www. kestrel. edu\/ java"},{"key":"3_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-44555-2_4","volume-title":"Object-Oriented Technology. ECOOP 2000 Workshop Reader","author":"S. Drossopoulou","year":"2000","unstructured":"S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter. Formal techniques for Java programs. In Jacques Malenfant, Sabine Moisan, and Ana Moreira, editors, Object-Oriented Technology. ECOOP 2000 Workshop Reader, volume 1964 of Lecture Notes in Computer Science, pages 41\u201354. Springer-Verlag, 2000."},{"key":"3_CR10","unstructured":"S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter, editors. Formal Techniques for Java Programs. Technical Report 269, Fernuniversit\u00e4t Hagen, 2000. Available from http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html ."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"S. Drossopoulou, S. Eisenbach, G. T. Leavens, P. M\u00fcller, A. Poetzsch-Heffter, and E. Poll. Formal techniques for Java programs. Available from http:\/\/www.informatik.fernuni-hagen.de\/import\/pi5\/workshops\/ecoop2001_papers.html , 2001.","DOI":"10.1007\/3-540-36208-8_19"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"S. Eisenbach. Formal underpinnings of Java. Workshop report, 1998. Available from http:\/\/www-dse.doc.ic.ac.uk\/~sue\/oopsla\/cfp.html .","DOI":"10.1145\/346852.346968"},{"key":"3_CR13","unstructured":"K. Huizing and R. Kuiper. Reinforcing fragile base classes. Available in [DEL+01], 2001."},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Secure Internet Programming: Security Issues for Distributed and Mobile Objects","author":"M. Hennessy","year":"1999","unstructured":"M. Hennessy and J. Riely. Type-safe execution of mobile agents in anonymous networks. In Jan Vitek and Thomas Jensen, editors, Secure Internet Programming: Security Issues for Distributed and Mobile Objects, volume 1603 of Lecture Notes in Computer Science. Springer-Verlag, 1999."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java, a minimal core calculus for Java and GJ. OOPSLA\u2019 99 Conference Proceedings, pages 132\u2013146, October 1999.","DOI":"10.1145\/320385.320395"},{"key":"3_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46589-8_6","volume-title":"Object-Oriented Technology. ECOOP\u201999 Workshop Reader","author":"B. Jacobs","year":"1999","unstructured":"B. Jacobs, G. T. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter. Formal techniques for Java programs. In A. Moreira and D. Demeyer, editors, Object-Oriented Technology. ECOOP\u201999 Workshop Reader, volume 1743 of Lecture Notes in Computer Science. Springer-Verlag, 1999."},{"key":"3_CR17","unstructured":"P. K\u00fcngas, V Kotkas, and Enn Tyugu. Introducing meta-interfaces into Java. Available in [DEL+01], 2001."},{"key":"3_CR18","unstructured":"G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06p, Iowa State University, Department of Computer Science, August 2001. See http:\/\/www.cs.iastate.edu\/~leavens\/JML.html ."},{"key":"3_CR19","unstructured":"K. R. M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03."},{"key":"3_CR20","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1990","unstructured":"C. Morgan. Programming from Specifications. Prentice Hall International, Hempstead, UK, 1990."},{"key":"3_CR21","unstructured":"P. M\u00fcller and A. Poetzsch-Heffter. A type system for controlling representation exposure in Java. Published in [DEJ+00b], 2000."},{"key":"3_CR22","unstructured":"P. M\u00fcller and A. Poetzsch-Heffter. A type system for checking applet isolation in Java Card. Available in [DEL+01], 2001."},{"key":"3_CR23","unstructured":"P. M\u00fcller, A. Poetzsch-Heffter, and G. T. Leavens. Modular specification of frame properties in JML. Available in [DEL+01], 2001."},{"key":"3_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BFb0054099","volume-title":"ECOOP\u2019 98 \u2014 Object-Oriented Programming, 12th European Conference, Brussels, Proceedings","author":"L. Mikhajlov","year":"1998","unstructured":"L. Mikhajlov and E. Sekerinski. A study of the fragile base class problem. In Eric Jul, editor, ECOOP\u2019 98 \u2014 Object-Oriented Programming, 12th European Conference, Brussels, Proceedings, volume 1445 of Lecture Notes in Computer Science, pages 355\u2013382. Springer-Verlag, July 1998."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen, 2001.","DOI":"10.1007\/3-540-45651-1"},{"key":"3_CR26","unstructured":"C. Pahl. Formalising dynamic composition and evolution in Java systems. Available in [DEL+01], 2001."},{"key":"3_CR27","unstructured":"M. Skoglund and T. Wrigstad. A mode system for read-only references in Java. Available in [DEL+01], 2001."},{"key":"3_CR28","unstructured":"J. van den Berg, C.-B. Breunesse, B. Jacobs, and E. Poll. On the role of invariants in reasoning about object-oriented languages. Available in [DEL+01], 2001."},{"key":"3_CR29","unstructured":"M. Viroli. From FGJ to Java according to LM translator. Available in [DEL+01], 2001."}],"container-title":["Lecture Notes in Computer Science","Object-Oriented Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47853-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T04:40:34Z","timestamp":1737348034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47853-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436751","9783540478539"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-47853-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"4 July 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}