{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T23:07:07Z","timestamp":1764284827439,"version":"3.46.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032120854"},{"type":"electronic","value":"9783032120861"}],"license":[{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-12086-1_3","type":"book-chapter","created":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T08:36:25Z","timestamp":1764146185000},"page":"39-60","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bridging the\u00a0B-Method and\u00a0ACSL: Towards Verified C Code"],"prefix":"10.1007","author":[{"given":"Fagner M.","family":"Dias","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcel V. M.","family":"Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,27]]},"reference":[{"key":"3_CR1","unstructured":"Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005)"},{"key":"3_CR2","unstructured":"Acsl importer (2025). https:\/\/frama-c.com\/fc-plugins\/acsl-importer.html"},{"key":"3_CR3","unstructured":"Arce, I., et al.: Avoiding the top 10 software security design flaws. IEEE Computer Society Center for Secure Design, Tech. rep. (2014)"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"3_CR5","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language \u2013 Version 1.20. Tech. rep., CEA LIST and INRIA Saclay (March 2009)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M.: Modular verification of jml contracts using bounded model checking. In: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part I 9, pp. 60\u201380. Springer (2020)","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Blanchard, A., Bobot, F., Baudin, P., Correnson, L.: Formally verifying that a program does what it should: The wp plug-in. In: Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, pp. 187\u2013261. Springer (2024)","DOI":"10.1007\/978-3-031-55608-1_4"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-58298-2_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Butler","year":"2020","unstructured":"Butler, M., K\u00f6rner, P., Krings, S., Lecomte, T., Leuschel, M., Mejia, L.F., Voisin, L.: The first twenty-five years of industrial use of the b-method. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) Formal Methods for Industrial Critical Systems, pp. 189\u2013209. Springer International Publishing, Cham (2020)"},{"key":"3_CR9","unstructured":"ClearSy: Atelier b. https:\/\/www.atelierb.eu\/en\/ (2025). Accessed 14 July 2025"},{"key":"3_CR10","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)"},{"key":"3_CR11","unstructured":"Significant cyber incidents. https:\/\/www.csis.org\/programs\/strategic-technologies-program\/significant-cyber-incidents. Accessed 29 July 2023"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15\u201329. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_10","DOI":"10.1007\/978-3-540-30482-1_10"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The why\/krakatoa\/caduceus platform for deductive program verification: (tool paper). In: International Conference on Computer Aided Verification, pp. 173\u2013177. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323\u2013338. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_20","DOI":"10.1007\/978-3-319-10181-1_20"},{"key":"3_CR16","unstructured":"Ge, N., Dieumegard, A., Jenn, E., Voisin, L.: From event-b to verified c via hll. arXiv preprint arXiv:1610.07410 (2016)"},{"issue":"3","key":"3_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. (CSUR) 44(3), 1\u201358 (2012)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"9","key":"3_CR18","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1378727.1378742","volume":"51","author":"M Hinchey","year":"2008","unstructured":"Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Commun. ACM 51(9), 54\u201359 (2008)","journal-title":"Commun. ACM"},{"issue":"3","key":"3_CR19","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"3_CR20","unstructured":"Leavens, G.T., et\u00a0al.: Jml reference manual (2008)"},{"key":"3_CR21","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., et\u00a0al.: Compcert - a formally verified optimizing compiler. In: 2016 ERTS Congress (Embedded Real Time Software and Systems), pp.\u00a01\u20138. SEE, SEE (January 2016)"},{"key":"3_CR22","unstructured":"Martin, D.: 11 of the most costly software errors in history. https:\/\/raygun.com\/blog\/costly-software-errors-history\/ (2014)"},{"key":"3_CR23","unstructured":"Schneider, S.: The B-Method: An Introduction. Palgrave Macmillan (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-12086-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T23:02:06Z","timestamp":1764284526000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-12086-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,27]]},"ISBN":["9783032120854","9783032120861"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-12086-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,27]]},"assertion":[{"value":"27 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Recife","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sbmf2025.ufrpe.br\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}