{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:14:06Z","timestamp":1725484446288},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540415138"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-44555-2_4","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T05:15:08Z","timestamp":1180329308000},"page":"41-54","source":"Crossref","is-referenced-by-count":6,"title":["Formal Techniques for Java Programs"],"prefix":"10.1007","author":[{"given":"Sophia","family":"Drossopoulou","sequence":"first","affiliation":[]},{"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"1Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"I. Attali, D. Caromel, H. Nilsson, and M. Russo. From executable formal specification to Java property verification. Published in [DEJ+00], 2000."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions. Published in [DEJ+00], 2000.","DOI":"10.1145\/504282.504284"},{"key":"4_CR3","unstructured":"D. Ancona. Available papers. Available from http:\/\/www.disi.unige.it\/person\/ AnconaD\/Publications.html , 2000."},{"key":"4_CR4","unstructured":"D. Ancona, E. Zucca, and S. Drossopoulou. Overloading and inheritance in java. Published in [DEJ+00], 2000."},{"key":"4_CR5","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Sousa, and S. Yu. Formalization in Coq of the Java Card Virtual Machine.Published in [DEJ+00], 2000."},{"key":"4_CR6","unstructured":"B. Beckert. A dynamic logic for Java Card. Published in [DEJ+00], 2000."},{"key":"4_CR7","unstructured":"J. van den Berg, E. Poll, and B. Jacobs. First steps in formalising JML. Published in [DEJ+00], 2000."},{"key":"4_CR8","unstructured":"P. Brisset. A case study in java software verification. Published in [DEJ+00], 2000."},{"key":"4_CR9","unstructured":"P. Cenciarelli. Event structures for Java. Published in [DEJ+00], 2000."},{"key":"4_CR10","unstructured":"P. Cenciarelli. The Java memory model. Available from http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/ , 2000."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"A. Coglio and A. Goldberg. Type safety in the jvm: Some problems in jdk 1.2.2 and proposed solutions. Published in [DEJ+00], 2000.","DOI":"10.1002\/cpe.596"},{"key":"4_CR12","unstructured":"A. Cavalcanti and D. Naumann. Simulation and class refinement for java. Published in [DEJ+00], 2000."},{"key":"4_CR13","unstructured":"E.-S. Cho and K. Yi. Escape analysis for stack allocation in java. Published in [DEJ+00], 2000."},{"key":"4_CR14","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.A vailable from http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html ."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"R. Diaconescu and K. Futatsugi. CafeOBJ report. World Scientific, 1999.","DOI":"10.1142\/3831"},{"key":"4_CR16","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":"4_CR17","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"4_CR18","series-title":"Lect Notes Comput Sci","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":"M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in Lecture Notes in Computer Science, pages 284\u2013303. Springer, Berlin, 2000."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes (preliminary report). In OOPSLA\u201998 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 329\u2013340.ACM, October 1998.","DOI":"10.1145\/286942.286973"},{"key":"4_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Formal techniques for Java programs","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":"4_CR21","unstructured":"V. Kotrajaras and S. Eisenbach. A demonstration of data inconsistency in the Java memory model. Published in [DEJ+00], 2000."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"G. Klein and T. Nipkow. Verified lightweight bytecode verification. Published in [DEJ+00], 2000.","DOI":"10.1002\/cpe.597"},{"key":"4_CR23","unstructured":"V. Kotrajaras. Vishnu\u2019s page. Available from http:\/\/www-dse.doc.ic.ac.uk\/~vk1\/ , 2000."},{"key":"4_CR24","first-page":"789","volume-title":"Handbook of Theoretical Computer Science","author":"D. Kozen","year":"1990","unstructured":"D. Kozen and J. Tiuryn. Logics of programs. In J. van Leewen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789\u2013840. The MIT Press, New York, NY, 1990."},{"key":"4_CR25","unstructured":"G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06k, Iowa State University, Department of Computer Science, July 2000. See http:\/\/www.cs.iastate.edu\/~leavens\/JML.html ."},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/PL00003926","volume":"10","author":"G. T. Leavens","year":"1998","unstructured":"G. T. Leavens and J. M. Wing. Protective interface specifications. Formal Aspects of Computing, 10:59\u201375, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"4_CR27","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 2nd edition, 1999."},{"key":"4_CR28","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"B. Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.","edition":"second edition"},{"key":"4_CR29","unstructured":"P. M\u00fcller and A. Poetzsch-Heffter. A type system for controlling representation exposure in Java. Published in [DEJ+00], 2000."},{"issue":"4","key":"4_CR30","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/261640.261641","volume":"6","author":"A. Moormann Zaremski","year":"1997","unstructured":"A. Moormann Zaremski and J. M. Wing. Specification matching of software components. ACM Transactions on Software Engineering and Methodology, 6(4):333\u2013369, October 1997.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"4_CR31","unstructured":"A. Nakagawa. Provers for behavioural logics: Combining model checking with deduction. Published in [DEJ+00], 2000."},{"key":"4_CR32","unstructured":"D. von Oheimb. Axiomatic semantics for Javalight. Published in [DEJ+00], 2000."},{"key":"4_CR33","unstructured":"D. von Oheimb. Axiomatic semantics for Javalight in Isabelle\/ HOL. Technical Report CSE 00-009, Oregon Graduate Institute, 2000. TPHOLS 2000 Supplemental Proceedings; available at http:\/\/isabelle.in.tum.de\/Bali\/ papers\/TPHOLs00.html ."},{"key":"4_CR34","unstructured":"M. O\u2019Cinneide and P. Nixon. Composite refactorings for Java Programs. Published in [DEJ+00], 2000."},{"key":"4_CR35","series-title":"Lect Notes Comput Sci","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":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S. D. Swierstra, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 162\u2013176. Springer, Berlin, 1999."},{"key":"4_CR36","unstructured":"E. Rose and K. H\u00f8gsbro Rose. Java access protection through typing. Published in [DEJ+00], 2000."},{"key":"4_CR37","unstructured":"E. Rose and K. Rose. Lightweight bytecode verification. In OOPSLA\u2019 98 Workshop, Formal Underpinnings fo Java, 1998."},{"key":"4_CR38","unstructured":"M. Russo. Java semantics: Formal semantics and interactive environment for parallel object-oriented programming. Available from http:\/\/www-sop.inria.fr\/ oasis\/personnel\/Marjorie.Russo\/java\/ , 2000."},{"key":"4_CR39","unstructured":"S. Skevoulis. A formal methods based static analysis approach for detecting runtime errors in java programs. Published in [DEJ+00], 2000."},{"key":"4_CR40","unstructured":"D. Wragg. Formal models of linking and binary compatibility. Published in [DEJ+00], 2000."}],"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-44555-2_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:14Z","timestamp":1605647174000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44555-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540415138"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-44555-2_4","relation":{},"subject":[]}}