{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:41:33Z","timestamp":1725540093448},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642049118"},{"type":"electronic","value":"9783642049125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04912-5_2","type":"book-chapter","created":{"date-parts":[[2009,10,26]],"date-time":"2009-10-26T11:04:31Z","timestamp":1256555071000},"page":"2-19","source":"Crossref","is-referenced-by-count":7,"title":["Teaching Formal Methods for the Unconquered Territory"],"prefix":"10.1007","author":[{"given":"Nestor","family":"Catano","sequence":"first","affiliation":[]},{"given":"Camilo","family":"Rueda","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","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":"2_CR2","unstructured":"Abrial, J.-R.: Rodin deliverable D7, Event-B mathematical Language. In: Information Society Technologies, ch.\u00a0V (2005)"},{"issue":"1-2","key":"2_CR3","first-page":"1","volume":"77","author":"J.-R. Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundam. Inf.\u00a077(1-2), 1\u201328 (2007)","journal-title":"Fundam. Inf."},{"issue":"1,2","key":"2_CR4","first-page":"1","volume":"77","author":"J.R. Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Informatica\u00a077(1,2), 1\u201324 (2007)","journal-title":"Fundamentae Informatica"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bouquet, F., Dadeau, F., Julien, J.: JML2B: Checking JML specifications with B machines. In: The 7th International B Conference, pp. 285\u2013288 (2007)","DOI":"10.1007\/11955757_31"},{"issue":"1\u20133","key":"2_CR6","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., Catano, N., Huisman, M., Jacobs, B.: Formal methods for Smart Cards: An experience report. Science of Computer Programming\u00a055(1\u20133), 53\u201380 (2005)","journal-title":"Science of Computer Programming"},{"issue":"3","key":"2_CR7","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","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. International Journal on Software Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Catano, N., Barraza, F., Garc\u00eda, D., Ortega, P., Rueda, C.: A case study in JML-assisted software development. In: Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008). ENTCS, July 2009, vol.\u00a0240, pp. 5\u201321 (2009)","DOI":"10.1016\/j.entcs.2009.05.042"},{"key":"2_CR9","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML reference manual (2008), http:\/\/www.eecs.ucf.edu\/~leavens\/-JML\/jmlrefman\/jmlrefman_toc.html"},{"key":"2_CR10","volume-title":"Unit Testing in Java","author":"J. Link","year":"2003","unstructured":"Link, J.: Unit Testing in Java. Morgan Kaufmann, San Francisco (2003)"},{"issue":"10","key":"2_CR11","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. Computer\u00a025(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"2_CR12","volume-title":"Object Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object Oriented Software Construction. Prentice Hall PTR, Englewood Cliffs (1997)"},{"key":"2_CR13","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI (November 2006)"},{"key":"2_CR14","volume-title":"Handbook of Automated Reasoning","author":"A. Robinson","year":"2001","unstructured":"Robinson, A., Voronkov, A.: Handbook of Automated Reasoning. MIT Press, Cambridge (2001)"},{"key":"2_CR15","volume-title":"The B-Method: An Introduction","author":"S. Schneider","year":"2001","unstructured":"Schneider, S.: The B-Method: An Introduction. Palgrave, Oxford (2001)"},{"issue":"1","key":"2_CR16","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1049\/sej.1989.0006","volume":"4","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: An introduction to Z and formal specifications. Software Engineering Journal\u00a04(1), 40\u201350 (1989)","journal-title":"Software Engineering Journal"},{"key":"2_CR17","series-title":"International Series in Computer Science","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Inc., Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Teaching Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04912-5_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:25Z","timestamp":1606185925000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04912-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642049118","9783642049125"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04912-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}