{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:08Z","timestamp":1725511868092},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712886"},{"type":"electronic","value":"9783540712893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71289-3_18","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T20:03:44Z","timestamp":1183493024000},"page":"215-229","source":"Crossref","is-referenced-by-count":9,"title":["Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode"],"prefix":"10.1007","author":[{"given":"Lilian","family":"Burdy","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Mariela","family":"Pavlova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"18_CR2","unstructured":"Alagi\u0107, S., Royer, M.: Next generation of virtual platforms. Article in odbms.org (2005), Available from http:\/\/odbms.org\/about_contributors_alagic.html"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-540-30142-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M.O., Loidl, H.-W., Momigliano, A.: A Program Logic for Resource Verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 34\u201349. Springer, Heidelberg (2004)"},{"key":"18_CR4","series-title":"ENTCS","first-page":"255","volume-title":"Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE)","author":"F.Y. Bannwart","year":"2005","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE). ENTCS, vol.\u00a0141, pp. 255\u2013273. Elsevier, Amsterdam (2005)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof Obligations Preserving Compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 112\u2013126. Springer, Heidelberg (2006)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/11924661_24","volume-title":"Programming Languages and Systems","author":"L. Beringer","year":"2006","unstructured":"Beringer, L., Hofmann, M.O.: A Bytecode Logic for JML and Types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 389\u2013405. Springer, Heidelberg (2006)"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.05.011","volume":"55","author":"C. Breunesse","year":"2005","unstructured":"Breunesse, C., Cata\u00f1o, N., Huisman, M., Jacobs, B.: Formal methods for smart cards: an experience report. Science of Computer Programming\u00a055, 53\u201380 (2005)","journal-title":"Science of Computer Programming"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. STTT\u00a07(3) (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"18_CR10","volume-title":"Proceedings of SAC\u201906","author":"L. Burdy","year":"2006","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Liebrock, L.M. (ed.) Proceedings of SAC\u201906, ACM Press, New York (2006)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: a Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/11513988_14","volume-title":"Computer Aided Verification","author":"A. Chander","year":"2005","unstructured":"Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.C.: JVer: A Java Verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 144\u2013147. Springer, Heidelberg (2005)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"18_CR14","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Sun Microsystems, Inc. (2005)"},{"key":"18_CR15","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J.: JML reference manual (2005), http:\/\/www.cs.iastate.edu\/~leavens\/JML\/jmlrefman\/jmlrefman_toc.html"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL (2007)","DOI":"10.1016\/j.entcs.2007.02.059"},{"key":"18_CR17","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Sun Microsystems, Inc. (1999)"},{"key":"18_CR18","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd rev. edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"18_CR19","unstructured":"Pavlova, M.: Specification and verification of Java bytecode. PhD thesis, Universit\u00e9 de Nice Sophia-Antipolis (2007)"},{"key":"18_CR20","unstructured":"Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report TR #00-03e, Department of Computer Science, Iowa State University (2000), Current revision from May 2005."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71289-3_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:17:58Z","timestamp":1605763078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71289-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712886","9783540712893"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71289-3_18","relation":{},"subject":[]}}