{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T15:49:45Z","timestamp":1762271385519,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642041662"},{"type":"electronic","value":"9783642041679"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04167-9_14","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T06:45:02Z","timestamp":1250664302000},"page":"278-297","source":"Crossref","is-referenced-by-count":5,"title":["BML and Related Tools"],"prefix":"10.1007","author":[{"given":"Jacek","family":"Chrz\u0105szcz","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Aleksy","family":"Schubert","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","first-page":"247","volume-title":"Logic in Computer Science","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Halpern, J. (ed.) Logic in Computer Science, p. 247. IEEE Press, Los Alamitos (2001); Invited Talk"},{"key":"14_CR2","volume-title":"Principles of Programming Languages","author":"A.W. Appel","year":"2000","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Principles of Programming Languages. ACM Press, New York (2000)"},{"key":"14_CR3","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":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-74792-5_7","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Burdy, L., Charles, J., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L., Pavlova, M.I., Requet, A.: JACK: A tool for validation of security and behaviour of Java applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol.\u00a04709, pp. 152\u2013174. Springer, Heidelberg (2007)"},{"key":"14_CR5","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":"14_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol.\u00a061. Springer, Heidelberg (1978)"},{"key":"14_CR7","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"73","volume-title":"Workshop on Formal Methods for Industrial Critical Systems","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a080, pp. 73\u201389. Elsevier, Amsterdam (2003)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-71289-3_18","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Burdy","year":"2007","unstructured":"Burdy, L., Huisman, M., Pavlova, M.I.: Preliminary design of BML: A behavioral interface specification language for java bytecode. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 215\u2013229. Springer, Heidelberg (2007)"},{"key":"14_CR9","first-page":"1835","volume-title":"Symposium on Applied Computing","author":"L. Burdy","year":"2006","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Symposium on Applied Computing, pp. 1835\u20131839. ACM Press, New York (2006)"},{"key":"14_CR10","unstructured":"Chrz\u0105szcz, J., Huisman, M., Schubert, A., Kiniry, J., Pavlova, M., Poll, E.: BML Reference Manual. In: Progress. INRIA and University of Warsaw (December 2008), http:\/\/bml.mimuw.edu.pl"},{"key":"14_CR11","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Formal encoding of JML level 0 specifications in jive. Technical report, ETH Zurich, Annual Report of the Chair of Software Engineering (2007)"},{"key":"14_CR12","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)"},{"issue":"8","key":"14_CR13","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A Logic for the Java Modeling Language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"14_CR15","unstructured":"JSR\u00a0175 Expert Group. A metadata facility for the Java programming language. Java Specification Request 175, Java Community Process (September 2004) Final release"},{"key":"14_CR16","unstructured":"JSR\u00a0308 Expert Group. Annotations on Java types. Java Specification Request 308, Java Community Process (2007) (in progress)"},{"key":"14_CR17","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06y, Iowa State University (1998) (revised since then 2004)"},{"key":"14_CR18","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.: JML Reference Manual, Department of Computer Science, Iowa State University (February 2008), http:\/\/www.jmlspecs.org"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL. In: Huisman, M., Spoto, F. (eds.) Bytecode Semantics, Verification, Analysis and Transformation. ENTCS (2007)","DOI":"10.1016\/j.entcs.2007.02.059"},{"key":"14_CR20","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1996","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1996)"},{"key":"14_CR21","unstructured":"Mallo, O.J.: A translator from BML annotated Java bytecode to BoogiePL. Master\u2019s thesis, Software Component Technology Group, ETH Zrich (2007)"},{"key":"14_CR22","unstructured":"MOBIUS Consortium. Deliverable\u00a03.1: Bytecode specification language and program logic (2006), http:\/\/mobius.inria.fr"},{"key":"14_CR23","unstructured":"MOBIUS Consortium. Deliverable\u00a04.2: Certificates (2007), http:\/\/mobius.inria.fr"},{"key":"14_CR24","unstructured":"Object Management Group. Object Constraint Language. OMG Available Specification, Version 2.0 (May 2006)"},{"key":"14_CR25","unstructured":"Pavlova, M.: Java bytecode verification and its applications. Th\u00e9se de doctorat, sp\u00e9cialit\u00e9 informatique, Universit\u00e9 Nice Sophia Antipolis, France (January 2007)"},{"key":"14_CR26","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq. In: [22] (2006), http:\/\/mobius.inria.fr\/bicolano"},{"key":"14_CR27","series-title":"ENTCS","volume-title":"Bytecode 2008","author":"A. Schubert","year":"2008","unstructured":"Schubert, A., Chrz\u0105szcz, J., Batkiewicz, T., Paszek, J., W\u0105s, W.: Technical aspects of class specification in the byte code of Java language. In: Bytecode 2008. ENTCS. Elsevier, Amsterdam (2008)"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Schubert, A., Walukiewicz-Chrz\u0105szcz, D.: The non-interference protection in a bytecode program logic (submitted, 2009)","DOI":"10.1016\/j.entcs.2009.11.018"},{"key":"14_CR29","unstructured":"Sznuk, T.: Introduction of the proof-carrying code technique to Java class. Master\u2019s thesis, Institute of Informatics, The University of Warsaw (2008) (in Polish)"}],"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-642-04167-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T22:30:24Z","timestamp":1558477824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04167-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642041662","9783642041679"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04167-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}