{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:40:20Z","timestamp":1767984020515,"version":"3.49.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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-10794-7_22","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:23Z","timestamp":1763189003000},"page":"451-459","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Auto-Generating Visual Editors for\u00a0Formal Logics with\u00a0Blockly"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"first","affiliation":[]},{"given":"Peng","family":"Lu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6138-4229","authenticated-orcid":false,"given":"Vadim","family":"Malvone","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"issue":"5","key":"22_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Crockford, D.: The application\/JSON media type for javascript object notation (json). RFC 4627 (2006). https:\/\/www.rfc-editor.org\/rfc\/rfc4627","DOI":"10.17487\/rfc4627"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Czepa, C., Zdun, U.: How understandable are pattern-based behavioral constraints for novice software designers? ACM Trans. Softw. Eng. Methodol. 28(2) (2019). https:\/\/doi.org\/10.1145\/3306608","DOI":"10.1145\/3306608"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Davis, J.A., et al.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 63\u201377. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41010-9_5","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"22_CR6","unstructured":"Ferrando, A., Malvone, V.: Hands-on VITAMIN: A compositional tool for model checking of multi-agent systems. In: Alderighi, M., Baldoni, M., Baroglio, C., Micalizio, R., Tedeschi, S. (eds.) Proceedings of the 25th Workshop \u201cFrom Objects to Agents\u201d, Bard (Aosta), Italy, July 8-10, 2024. CEUR Workshop Proceedings, vol.\u00a03735, pp. 148\u2013160. CEUR-WS.org (2024). https:\/\/ceur-ws.org\/Vol-3735\/paper_12.pdf"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Ferrando, A., Malvone, V.: VITAMIN: a compositional framework for model checking of multi-agent systems. In: Rocha, A.P., Steels, L., van\u00a0den Herik, H.J. (eds.) Proceedings of the 17th International Conference on Agents and Artificial Intelligence, ICAART 2025 - Volume 1, Porto, Portugal, February 23\u201325, 2025, pp. 648\u2013655. SCITEPRESS (2025). https:\/\/doi.org\/10.5220\/0013349600003890","DOI":"10.5220\/0013349600003890"},{"key":"22_CR8","unstructured":"Ferrando, A., Malvone, V.: Vitamin: verification of a multi agent system. In: Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025, pp. 3023\u20133025. International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC (2025)"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Grobelna, I.: Scratch-based user-friendly requirements definition for formal verification of control systems. Informatics Educ. 19(2), 223\u2013238 (2020). https:\/\/doi.org\/10.15388\/infedu.2020.11","DOI":"10.15388\/infedu.2020.11"},{"key":"22_CR10","unstructured":"Harvey, B., M\u00f6nig, J.: Snap! a visual, drag-and-drop programming language. https:\/\/snap.berkeley.edu\/ (2013). Accessed Sept. 2025"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Jamroga, W., Malvone, V., Murano, A.: Natural strategic ability. Artif. Intell. 277 (2019). https:\/\/doi.org\/10.1016\/j.artint.2019.103170","DOI":"10.1016\/j.artint.2019.103170"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Mansoor, N., Bagheri, H., Kang, E., Sharif, B.: An empirical study assessing software modeling in alloy. In: 11th IEEE\/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2023, Melbourne, Australia, May 14\u201315, 2023, pp. 44\u201354. IEEE (2023). https:\/\/doi.org\/10.1109\/FormaliSE58978.2023.00013","DOI":"10.1109\/FormaliSE58978.2023.00013"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1\u201334:47 (2014)","DOI":"10.1145\/2631917"},{"key":"22_CR14","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-27668-7_7","volume-title":"Information Systems Security and Privacy","author":"H Nergaard","year":"2015","unstructured":"Nergaard, H., Ulltveit-Moe, N., Gj\u00f8s\u00e6ter, T.: ViSPE: a graphical policy editor for XACML. In: Camp, O., Weippl, E., Bidan, C., A\u00efmeur, E. (eds.) ICISSP 2015. CCIS, vol. 576, pp. 107\u2013121. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-27668-7_7"},{"issue":"4","key":"22_CR15","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1093\/logcom\/exv034","volume":"28","author":"HN Nguyen","year":"2018","unstructured":"Nguyen, H.N., Alechina, N., Logan, B., Rakib, A.: Alternating-time temporal logic with resource bounds. J. Log. Comput. 28(4), 631\u2013663 (2018). https:\/\/doi.org\/10.1093\/logcom\/exv034","journal-title":"J. Log. Comput."},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Omar, C., Voysey, I., Chugh, R., Hammer, M.A.: Live functional programming with typed holes. Proc. ACM Program. Lang. 3(POPL), 14:1\u201314:32 (2019). https:\/\/doi.org\/10.1145\/3290327","DOI":"10.1145\/3290327"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Pasternak, E., Fenichel, R., Marshall, A.N.: Tips for creating a block language with blockly. In: 2017 IEEE Blocks and Beyond Workshop (B &B), pp. 21\u201324 (2017). https:\/\/doi.org\/10.1109\/BLOCKS.2017.8120404","DOI":"10.1109\/BLOCKS.2017.8120404"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"22_CR19","doi-asserted-by":"publisher","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009)https:\/\/doi.org\/10.1145\/1592434.1592436","DOI":"10.1145\/1592434.1592436"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:27Z","timestamp":1767967167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}