{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:18Z","timestamp":1725558978795},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255598"},{"type":"electronic","value":"9783540320074"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11415787_25","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T18:07:36Z","timestamp":1278871656000},"page":"434-453","source":"Crossref","is-referenced-by-count":6,"title":["Checking JML Specifications with B Machines"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Bouquet","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Groslambert","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)"},{"key":"25_CR2","unstructured":"The B4free web site (2003), \n                  \n                    http:\/\/www.b4free.com"},{"key":"25_CR3","series-title":"ENTCS","first-page":"73","volume-title":"Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003)","author":"L. Burdy","year":"2003","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. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). ENTCS, vol.\u00a080, pp. 73\u201389. Elsevier, Amsterdam (2003)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-540-31980-1_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 551\u2013556. Springer, Heidelberg (2005) (to appear)"},{"key":"25_CR5","unstructured":"Bellegarde, F., Groslambert, J., Huisman, M., Kouchnarenko, O., Julliand, J.: Verification of liveness properties with JML. Technical Report RR-5331, INRIA (2004)"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/s001650070034","volume":"12","author":"R.-J. Back","year":"2000","unstructured":"Back, R.-J., Mikhajlova, A., von Wright, J.: Class refinement as semantics of correct object substitutability. Formal Aspects of Computing\u00a012, 18\u201340 (2000)","journal-title":"Formal Aspects of Computing"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"25_CR8","doi-asserted-by":"crossref","unstructured":"Couchot, J.-F., Dadeau, F., D\u00e9harbe, D., Giorgetti, A., Ranise, S.: Proving and debugging set-based specifications. In: proceedings of the Sixth Brazilian Workshop on Formal Methods (WMF 2003), May 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a095, pp. 189\u2013208 (2003)","DOI":"10.1016\/j.entcs.2004.04.012"},{"key":"25_CR9","unstructured":"Clearsy, Europarc de Pichaury 13856 Aix-en-Provence Cedex 3\u00a0- France. Atelier B Technical Support version 3 (May 2001), \n                  \n                    http:\/\/www.atelierb.societe.com"},{"key":"25_CR10","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification, 2nd edn. Java Series. Sun Microsystems (2000)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","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":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"25_CR12","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/3-540-45648-1_27","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"R. Laleau","year":"2002","unstructured":"Laleau, R., Polack, F.: Coming and going from UML to B: a proposal to support traceability in rigorous IS development. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 517\u2013534. Springer, Heidelberg (2002)"},{"key":"25_CR14","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"issue":"1-2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"25_CR16","unstructured":"Neilson, D., Sorensen, I.H.: The B-Technologies: a system for computer aided programming. B-Core (UK) Limited, Kings Piece, Harwell, Oxon, OX11 0PA (1999), \n                  \n                    http:\/\/www.b-core.com\/btoolkit.html"},{"key":"25_CR17","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. addison-wesley edition, Reading (1999)"},{"key":"25_CR18","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"J. Warmer","year":"1998","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1998)"}],"container-title":["Lecture Notes in Computer Science","ZB 2005: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11415787_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:53:00Z","timestamp":1558281180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11415787_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255598","9783540320074"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11415787_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}