{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T04:31:34Z","timestamp":1770352294783,"version":"3.49.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107619","type":"print"},{"value":"9783032107626","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-10762-6_23","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T16:08:19Z","timestamp":1763222899000},"page":"303-312","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Analysis of\u00a0a\u00a0Railway Signaling Block Designed in\u00a0AIDA"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Cavada","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Lidstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Gianluca","family":"Redondi","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Tessi","sequence":"additional","affiliation":[]},{"given":"Dylan","family":"Trenti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-030-61467-6_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"A Amendola","year":"2020","unstructured":"Amendola, A., et al.: A model-based approach to the design, verification and deployment of railway interlocking system. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 240\u2013254. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_16"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H.: Formal methods and tools applied in the railway domain. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds.) Rigorous State-Based Methods, LNCS, pp. 3\u201321. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_1","DOI":"10.1007\/978-3-031-63790-2_1"},{"key":"23_CR3","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification, LNCS, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"23_CR4","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: Automated parameterized verification of a railway protection system with dafny. In: Piskac, R., Rakamari\u0107, Z. (eds.) Computer Aided Verification. CAV 2025. LNCS, vol. 15934. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_17","DOI":"10.1007\/978-3-031-98685-7_17"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Griggio, A., Susi, A.: A formal IDE for railways: research challenges. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, pp. 107\u2013115. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-26236-4_9","DOI":"10.1007\/978-3-031-26236-4_9"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-030-79876-5_8","volume-title":"Automated Deduction \u2013 CADE 28","author":"A Cimatti","year":"2021","unstructured":"Cimatti, A., Griggio, A., Redondi, G.: Universal invariant checking of parametric systems with quantifier-free SMT reasoning. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 131\u2013147. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_8"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Redondi, G.: Towards the verification of a generic interlocking logic: dafny meets parameterized model checking. CoRR abs\/2403.00087 (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.00087","DOI":"10.48550\/arXiv.2403.00087"},{"key":"23_CR8","doi-asserted-by":"publisher","unstructured":"Cimatti, A., et al.: Model-based testing of railway interlocking systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Application Areas. ISoLA 2024. LNCS, vol. 15223, pp. 112\u2013126. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75390-9_8","DOI":"10.1007\/978-3-031-75390-9_8"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-13754-9_4","volume-title":"Time for Verification","author":"EM Clarke","year":"2010","unstructured":"Clarke, E.M., Kurshan, R.P., Veith, H.: The localization reduction and counterexample-guided abstraction refinement. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 61\u201371. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_4"},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Beek, M.H.T.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4) (2022). https:\/\/doi.org\/10.1145\/3520480","DOI":"10.1145\/3520480"},{"key":"23_CR11","doi-asserted-by":"publisher","unstructured":"Frenkel, E., Chajed, T., Padon, O., Shoham, S.: Efficient implementation of an abstract domain of quantified first-order formulas. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. CAV 2024. LNCS, vol. 14682, pp. 86\u2013108. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_5","DOI":"10.1007\/978-3-031-65630-9_5"},{"key":"23_CR12","doi-asserted-by":"publisher","unstructured":"Haxthausen, A.E., Fantechi, A.: Compositional verification of railway interlocking systems. Form. Asp. Comput. 35(1) (2023). https:\/\/doi.org\/10.1145\/3549736","DOI":"10.1145\/3549736"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-99130-6_7","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2018","unstructured":"Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Formal verification of Signalling programs with SafeCap. In: Gallina, B., Skavhaug, A., Bitsch, F. (eds.) SAFECOMP 2018. LNCS, vol. 11093, pp. 91\u2013106. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99130-6_7"},{"issue":"1","key":"23_CR14","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1109\/TDSC.2022.3141555","volume":"20","author":"A Iliasov","year":"2023","unstructured":"Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Practical verification of railway signalling programs. IEEE Trans. Dependable Secure Comput. 20(1), 695\u2013707 (2023). https:\/\/doi.org\/10.1109\/TDSC.2022.3141555","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Jin-hua, L., Qiong, L., Jing, L.: The W-model for testing software product lines. In: 2008 International Symposium on Computer Science and Computational Technology, vol. 1, pp. 690\u2013693 (2008). https:\/\/doi.org\/10.1109\/ISCSCT.2008.34","DOI":"10.1109\/ISCSCT.2008.34"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"4","key":"23_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3686153","volume":"25","author":"G Redondi","year":"2024","unstructured":"Redondi, G., Cimatti, A., Griggio, A., Mcmillan, K.L.: Invariant checking for SMT-based systems with quantifiers. ACM Trans. Comput. Log. 25(4), 1\u201337 (2024). https:\/\/doi.org\/10.1145\/3686153","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10762-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T16:23:38Z","timestamp":1764865418000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10762-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107619","9783032107626"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10762-6_23","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":"RSSRail","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reliability, Safety, and Security of Railway Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pisa","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","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":"rssrail2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rssrail2025.isti.cnr.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}