{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:28:24Z","timestamp":1743006504851,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031713781"},{"type":"electronic","value":"9783031713798"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-71379-8_6","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:02:25Z","timestamp":1725458545000},"page":"91-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Contracts in Event-B"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5231-6611","authenticated-orcid":false,"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,5]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT, 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","DOI":"10.1007\/s10009-010-0145-y"},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s001650300002","volume":"14","author":"J-R Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D., M\u00e9ry, D.: A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Formal Aspects Comput. 14(3), 215\u2013227 (2003)","journal-title":"Formal Aspects Comput."},{"key":"6_CR5","unstructured":"Barradas, H.-.: Event-B: syntax and proof oglogations in Atelier-B. Technical report, ClearSy (2020)"},{"issue":"8","key":"6_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-c software analysis platform. Commun. ACM 64(8), 56\u201368 (2021)","journal-title":"Commun. ACM"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Catano, N., Leino, K.R.M., Rivera, V.: The eventb2dafny Rodin plug-in. In: Garbervetsky, D., Kim, S., (eds.) Proceedings of the Second International Workshop on Developing Tools as Plug-Ins, TOPI 2012, Zurich, Switzerland, June 3, 2012, pp. 49\u201354. IEEE Computer Society (2012)","DOI":"10.1109\/TOPI.2012.6229810"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pp. 117\u2013126. ACM Press (1983)","DOI":"10.1145\/567067.567080"},{"key":"6_CR9","unstructured":"ClearSy. B Language reference manual ver.1.8.10 (2022)"},{"key":"6_CR10","unstructured":"Cousot, P.: Principles of Abstract Interpretation. The MIT Press (2021)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Calculational design of [in]correctness transformational program logics by abstract interpretation. Proc. ACM Program. Lang. 8(POPL), 175\u2013208 (2024)","DOI":"10.1145\/3632849"},{"key":"6_CR12","first-page":"75","volume-title":"Tools & Notions for Program Construction: an Advanced Course","author":"P Cousot","year":"1982","unstructured":"Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In: N\u00e9el, D. (ed.) Tools & Notions for Program Construction: an Advanced Course, pp. 75\u2013119. Cambridge University Press, Cambridge, UK (1982)"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-94-011-1793-7_4","volume-title":"Program Verification: Fundamental Issues in Computer Science","author":"RW Floyd","year":"1993","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification: Fundamental Issues in Computer Science, pp. 65\u201381. Springer, Netherlands, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4"},{"key":"6_CR14","unstructured":"Ford, R.L., Leino, K.R.M.: Dafny reference manual (2017)"},{"issue":"10","key":"6_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. In: Monahan, R., Prevosto, V., Proen\u00e7a, J. (eds.) Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019. EPTCS, vol. 310, pp. 50\u201362 (2019)","DOI":"10.4204\/EPTCS.310.6"},{"key":"6_CR17","unstructured":"Verimag Laboratory: the synchrone reactive toolbox (2022). https:\/\/www-verimag.imag.fr\/DIST-TOOLS\/SYNCHRONE\/reactive-toolbox\/"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR19","unstructured":"Maamria, I., Fathabadi, A.S.: Theory Plug-in User Manual. University of Southampton, 30 April 2014"},{"key":"6_CR20","volume-title":"Mathematical Theory of Computation","author":"Z Manna","year":"2003","unstructured":"Manna, Z.: Mathematical Theory of Computation. Dover Publications Inc, US (2003)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/3-540-56496-9_27","volume-title":"Computer Aided Verification","author":"D M\u00e9ry","year":"1993","unstructured":"M\u00e9ry, D., Mokkedem, A.: Crocos: an integrated environment for interactive verification of SDL specifications. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 343\u2013356. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_27"},{"key":"6_CR22","unstructured":"Meyer, B.: Design by contract. In:\u00a0Mandrioli, D.,\u00a0Meyer, B. (eds.) Advances in Object-Oriented Software Engineering, pp. 1\u201350 (1991)"},{"key":"6_CR23","unstructured":"Why3 Team. Why3. https:\/\/why3.lri.fr"},{"key":"6_CR24","unstructured":"Iowa University. Kind2 multi-engine SMT-based automatic model checker for synchronous reactive systems (2024). https:\/\/kind2-mc.github.io\/kind2\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods Teaching"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71379-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:02:56Z","timestamp":1725458576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71379-8_6"}},"subtitle":["Reporting the Introduction and the Use of Automated Tools for Verifying Software-Based Systems in Higher Education"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031713781","9783031713798"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71379-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMTea","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Formal Methods Teaching Workshop","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=423","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}