{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T20:24:11Z","timestamp":1792182251694,"version":"4.4.0"},"reference-count":188,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T00:00:00Z","timestamp":1784592000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,9,30]]},"abstract":"<jats:p>The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this article, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B\u00a0method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.<\/jats:p>","DOI":"10.1145\/3802545","type":"journal-article","created":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T21:08:48Z","timestamp":1773781728000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A History of Formal Methods in Railways"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[{"name":"CNR-ISTI","place":["Pisa, Italy"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"University of Florence","place":["Florence, Italy"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0636-5663","authenticated-orcid":false,"given":"Alessio","family":"Ferrari","sequence":"additional","affiliation":[{"name":"University College Dublin","place":["Dublin, Ireland"]},{"name":"CNR-ISTI","place":["Dublin, Ireland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[{"name":"CNR-ISTI","place":["Pisa, Italy"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7349-8872","authenticated-orcid":false,"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[{"name":"Technical University of Denmark","place":["Lyngby, Denmark"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8977-4827","authenticated-orcid":false,"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[{"name":"CLEARSY Systems Engineering","place":["Aix-en-Provence, France"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,21]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134406"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-013-05-0619"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00525-3"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-015-5346-2"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_7"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3054-3_33"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00539-x"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/RE59067.2024.00031"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-23008-0"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_20"},{"key":"e_1_3_3_15_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, USA. Retrieved from https:\/\/mitpress.mit.edu\/9780262026499\/principles-of-model-checking\/"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2017.2681076"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00244-2_7"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00556-1"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00653-3"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_46"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3702231"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689374"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-73887-6_21"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.002"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_22"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43681-9_2"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_32_2","first-page":"20","volume-title":"Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u201903)","author":"Bj\u00f8rner Dines","year":"2003","unstructured":"Dines Bj\u00f8rner. 2003. New results and trends in formal techniques and tools for the development of software for transportation systems: A review. In Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u201903), G\u00e9za Tarnai and Eckehard Schnieder (Eds.). L\u2019Harmattan, Hungary, 20 pages. Retrieved from http:\/\/www.imm.dtu.dk\/dibj\/dines-amore.pdf"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_4"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.004"},{"key":"e_1_3_3_35_2","first-page":"8","article-title":"25 Years of Formal Methods at RATP: From Manual Approach for Proof of Programs to Instrumented Demonstration of Railway Systems Safety","author":"Bonvoisin David","year":"2016","unstructured":"David Bonvoisin. 2016. 25 Years of Formal Methods at RATP: From Manual Approach for Proof of Programs to Instrumented Demonstration of Railway Systems Safety. International Railway Safety Council Meeting (IRSC\u201916), 8 pages. Retrieved from https:\/\/international-railway-safety-council.com\/wp-content\/uploads\/2017\/09\/bonvoisin-25-years-of-formal-methods-at-ratp.pdf","journal-title":"International Railway Safety Council Meeting (IRSC\u201916)"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_3"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/S001650050021"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_39"},{"key":"e_1_3_3_39_2","first-page":"6","article-title":"Holistic Study of Formal Methods and Standardization in Specification, Development, Verification and Validation of Railway Signalling System Software","author":"Bor\u00e4lv Arne","year":"2022","unstructured":"Arne Bor\u00e4lv, Randolf Berglehner, Ibtihel Cherif, Daniel Fredholm, Dominik Hansen, Javier Magro, Luis-Fernando Mejia, David Mentr\u00e9, Abdul Rasheeq, Daniel Schwencke, et\u00a0al. 2022. Holistic Study of Formal Methods and Standardization in Specification, Development, Verification and Validation of Railway Signalling System Software. 13th World Congress on Railway Research (WCRR\u201922), 6 pages. Retrieved from https:\/\/www.researchgate.net\/profile\/Arne-Boralv\/publication\/363535915_Holistic_study_of_Formal_Methods_and_Standardization_in_development_verification_and_validation_of_railway_signalling_system_software\/links\/63217f59873eca0c00872c32\/Holistic-study-of-Formal-Methods-and-Standardization-in-development-verification-and-validation-of-railway-signalling-system-software.pdf","journal-title":"13th World Congress on Railway Research (WCRR\u201922)"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2014.11.007"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118561829"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118561829"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781119002727"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3528207"},{"key":"e_1_3_3_45_2","volume-title":"Computing Handbook","author":"Bowen Jonathan P.","year":"2014","unstructured":"Jonathan P. Bowen and Michael G. Hinchey. 2014. Formal methods. In Computing Handbook, Teofilo F. Gonzalez, Jorge Diaz-Herrera, and Allen Tucker (Eds.). CRC, USA, Chapter 71, 71\u201325."},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024646"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_17"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3670795"},{"key":"e_1_3_3_49_2","first-page":"3","volume-title":"Proceedings of the FM\u201999 B Users Group Meeting on Applying B in an industrial context: Tools, Lessons and Techniques (BUGM\u201999)","author":"Burdy Lilian","year":"1999","unstructured":"Lilian Burdy and Jean-Marc Meynadier. 1999. Automatic refinement. In Proceedings of the FM\u201999 B Users Group Meeting on Applying B in an industrial context: Tools, Lessons and Techniques (BUGM\u201999). 3\u201315. Retrieved from https:\/\/www-sop.inria.fr\/everest\/personnel\/Lilian.Burdy\/ug020003.pdf"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)38145-4"},{"key":"e_1_3_3_51_2","volume-title":"Rapport d\u2019enqu\u00eate technique sur la survitesse d\u2019un TGV \u00e0 La Milesse (72) le 22 d\u00e9cembre 2019","author":"(BEA-TT) Bureau d\u2019Enqu\u00eates sur les Accidents de Transport Terrestre","year":"2021","unstructured":"Bureau d\u2019Enqu\u00eates sur les Accidents de Transport Terrestre (BEA-TT). 2021. Rapport d\u2019enqu\u00eate technique sur la survitesse d\u2019un TGV \u00e0 La Milesse (72) le 22 d\u00e9cembre 2019. Technical Report EQ-BEAT\u201321-6\u2013FR. BEA-TT. Retrieved from https:\/\/www.bea-tt.developpement-durable.gouv.fr\/IMG\/pdf\/rapport_beatt_2020_01.pdfIn French."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00562-3"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_8"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68499-4_5"},{"key":"e_1_3_3_55_2","article-title":"The Impact of EN 50716 on Rail Digitalization and Advanced Technologies","author":"Camacho Ricardo","year":"2025","unstructured":"Ricardo Camacho. 2025. The Impact of EN 50716 on Rail Digitalization and Advanced Technologies. Parasoft blog. Retrieved from https:\/\/www.parasoft.com\/blog\/en-50716-impact-on-rail-digitalization\/","journal-title":"Parasoft blog"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71374-4_1"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2025\/1155"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810312"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/S001650050022"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-009-0130-7"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377659"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68499-4_10"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_13"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.345825"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-0-20452-1"},{"key":"e_1_3_3_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00540-4"},{"key":"e_1_3_3_71_2","series-title":"IFIP Transactions","first-page":"199","volume-title":"Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992)","volume":"10","author":"DaSilva Clara","year":"1992","unstructured":"Clara DaSilva, Babak Dehbonei, and Fernando Mejia. 1992. Formal specification in the development of industrial applications: Subway speed control system. In Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992)(IFIP Transactions, Vol. C-10), Michel Diaz and Roland Groz (Eds.). North-Holland, The Netherlands, 199\u2013213."},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-014-0361-Y"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00548-w"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.3166\/tsi.22.11-32"},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3670419"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-77792-9_12"},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100063"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/11955757_21"},{"key":"e_1_3_3_81_2","unstructured":"European Committee for Electrotechnical Standardization. 2011. CENELEC EN 50128: Railway applications \u2013 Communication signalling and processing systems \u2013 Software for railway control and protection systems. Retrieved from https:\/\/standards.globalspec.com\/std\/14317747\/en-50128"},{"key":"e_1_3_3_82_2","unstructured":"European Committee for Electrotechnical Standardization. 2017. CENELEC EN 50657: Railway Applications \u2013 Rolling stock applications \u2013 Software on Board Rolling Stock. Retrieved from https:\/\/standards.globalspec.com\/std\/10182637\/en-50657"},{"key":"e_1_3_3_83_2","unstructured":"European Committee for Electrotechnical Standardization. 2018. CENELEC EN 50129: Railway applications \u2013 Communication signalling and processing systems \u2013 Safety related electronic systems for signalling. Retrieved from https:\/\/standards.globalspec.com\/std\/13113133\/en-50129"},{"key":"e_1_3_3_84_2","unstructured":"European Committee for Electrotechnical Standardization. 2023. CENELEC EN 50716: Railway Applications \u2013 Requirements for software development. Retrieved from https:\/\/standards.globalspec.com\/std\/14648351\/en-50716"},{"key":"e_1_3_3_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33170-1_4"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2015.2446985"},{"key":"e_1_3_3_87_2","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-4666-1643-1.ch012"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05032-4_13"},{"key":"e_1_3_3_89_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898.ch4"},{"key":"e_1_3_3_90_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_24"},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19762-8_19"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75390-9_7"},{"key":"e_1_3_3_93_2","doi-asserted-by":"publisher","DOI":"10.1109\/REW61692.2024.00044"},{"key":"e_1_3_3_94_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.44"},{"key":"e_1_3_3_95_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.04.003"},{"key":"e_1_3_3_96_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"e_1_3_3_97_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3124677"},{"key":"e_1_3_3_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380373"},{"key":"e_1_3_3_99_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.INFSOF.2025.107697"},{"key":"e_1_3_3_100_2","doi-asserted-by":"publisher","DOI":"10.1145\/3520480"},{"key":"e_1_3_3_101_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_15"},{"key":"e_1_3_3_102_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2026.3661866"},{"key":"e_1_3_3_103_2","first-page":"101","volume-title":"Proceedings of the 5th Conference on Computers in Railways (COMPRAIL\u201996)","author":"Fokkink Wan F.","year":"1996","unstructured":"Wan F. Fokkink. 1996. Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In Proceedings of the 5th Conference on Computers in Railways (COMPRAIL\u201996), Vol. I: Railway Systems and Management. Computational Mechanics Publications, Germany, 101\u2013110."},{"key":"e_1_3_3_104_2","volume-title":"Formal Methods for Safe and Secure Computer Systems","author":"Garavel Hubert","year":"2013","unstructured":"Hubert Garavel and Susanne Graf. 2013. Formal Methods for Safe and Secure Computer Systems. BSI Study 875. Bundesamt f\u00fcr Sicherheit in der Informationstechnik. Retrieved from https:\/\/www.bsi.bund.de\/SharedDocs\/Downloads\/DE\/BSI\/Publikationen\/Studien\/formal_methods_study_875\/formal_methods_study_875.html"},{"key":"e_1_3_3_105_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_3_3_106_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_3_107_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1994.1279941"},{"key":"e_1_3_3_108_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.251198"},{"key":"e_1_3_3_109_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2017.2657695"},{"key":"e_1_3_3_110_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"e_1_3_3_111_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898"},{"key":"e_1_3_3_112_2","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"e_1_3_3_113_2","doi-asserted-by":"publisher","DOI":"10.5555\/100296.100321"},{"key":"e_1_3_3_114_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.09.027"},{"key":"e_1_3_3_115_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00551-6"},{"key":"e_1_3_3_116_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33600-8_10"},{"key":"e_1_3_3_117_2","doi-asserted-by":"publisher","DOI":"10.1109\/WIFT.1995.515481"},{"key":"e_1_3_3_118_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21292-5_10"},{"key":"e_1_3_3_119_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34032-1_25"},{"key":"e_1_3_3_120_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12566-9_8"},{"key":"e_1_3_3_121_2","doi-asserted-by":"publisher","DOI":"10.1145\/3549736"},{"key":"e_1_3_3_122_2","first-page":"127","volume-title":"Railways: Types, Design and Safety Issues","author":"Haxthausen Anne E.","year":"2013","unstructured":"Anne E. Haxthausen and Jan Peleska. 2013. Efficient development and verification of safe railway control software. In Railways: Types, Design and Safety Issues, Cacilie Reinhardt and Klaus Shroeder (Eds.). Nova Science, USA, Chapter 5, 127\u2013148."},{"key":"e_1_3_3_123_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2021.06.049"},{"key":"e_1_3_3_124_2","doi-asserted-by":"publisher","DOI":"10.1109\/OJITS.2023.3267142"},{"key":"e_1_3_3_125_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2014.2366512"},{"key":"e_1_3_3_126_2","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann Gerard J.","year":"2003","unstructured":"Gerard J. Holzmann. 2003. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, USA."},{"key":"e_1_3_3_127_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_3_128_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICITE50838.2020.9231438"},{"key":"e_1_3_3_129_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3141555"},{"key":"e_1_3_3_130_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-014-0304-7"},{"key":"e_1_3_3_131_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47169-3_21"},{"key":"e_1_3_3_132_2","doi-asserted-by":"publisher","unstructured":"Adam Tauman Kalai Ofir Nachum Santosh S. Vempala and Edwin Zhang. 2025. Why Language Models Hallucinate. arxiv:2509.04664. DOI:10.48550\/arXiv.2509.04664","DOI":"10.48550\/arXiv.2509.04664"},{"key":"e_1_3_3_133_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58555-9_86"},{"key":"e_1_3_3_134_2","doi-asserted-by":"publisher","DOI":"10.1145\/3664191"},{"key":"e_1_3_3_135_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_32"},{"key":"e_1_3_3_136_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_3"},{"key":"e_1_3_3_137_2","first-page":"57","volume-title":"Proceedings of the 1st International Workshop about Sets and Tools (SETS\u201914)","author":"Lecomte Thierry","year":"2014","unstructured":"Thierry Lecomte. 2014. Return of experience on automating refinement in B. In Proceedings of the 1st International Workshop about Sets and Tools (SETS\u201914), David Delahaye and Catherine Dubois (Eds.). CNAM, France, 57\u201368. Retrieved from http:\/\/sets2014.cnam.fr\/papers\/00010057.pdf"},{"key":"e_1_3_3_138_2","doi-asserted-by":"publisher","unstructured":"Thierry Lecomte Lilian Burdy and Michael Leuschel. 2020. Formally Checking Large Data Sets in the Railways. arxiv:1210.6815. DOI:10.48550\/arXiv.1210.6815. Proceedings of the ICFEM\u201912 Workshop on the experience of and advances in developing dependable systems in Event-B (DS-Event-B\u201912).","DOI":"10.48550\/arXiv.1210.6815"},{"key":"e_1_3_3_139_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102524"},{"key":"e_1_3_3_140_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"e_1_3_3_141_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"e_1_3_3_142_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_3_143_2","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.76.1077"},{"key":"e_1_3_3_144_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2017.07.044"},{"key":"e_1_3_3_145_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00543-1"},{"key":"e_1_3_3_146_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2017.2658179"},{"key":"e_1_3_3_147_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47169-3_22"},{"key":"e_1_3_3_148_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3"},{"key":"e_1_3_3_149_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2011.2178238"},{"key":"e_1_3_3_150_2","first-page":"25","volume-title":"Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912)","author":"Miller Steven P.","year":"2012","unstructured":"Steven P. Miller. 2012. Lessons from twenty years of industrial formal methods. In Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912). Cyber-Physical Systems Virtual Organization, USA, 25 pages. Retrieved from http:\/\/cps-vo.org\/node\/3434"},{"key":"e_1_3_3_151_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2015.7295465"},{"key":"e_1_3_3_152_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_153_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0089-2"},{"key":"e_1_3_3_154_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_155_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-015-0374-1"},{"key":"e_1_3_3_156_2","volume-title":"Railway operation and control (4 ed.)","author":"Pachl J\u00f6rn","year":"2018","unstructured":"J\u00f6rn Pachl. 2018. Railway operation and control (4 ed.). VTD Rail Publishing, USA."},{"key":"e_1_3_3_157_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_14"},{"key":"e_1_3_3_158_2","series-title":"IFIP Transactions","first-page":"189","volume-title":"Proceedings of the 6th IFIP TC6\/WG6.1 International Conference on Formal Description Techniques (FORTE\u201993)","volume":"22","author":"Parkin Graeme I. P.","year":"1993","unstructured":"Graeme I. P. Parkin and Stephen Austin. 1993. Overview: Survey of formal methods in industry. In Proceedings of the 6th IFIP TC6\/WG6.1 International Conference on Formal Description Techniques (FORTE\u201993)(IFIP Transactions, Vol. C-22), Richard L. Tenney, Paul D. Amer, and M. \u00dcmit Uyar (Eds.). North-Holland, The Netherlands, 189\u2013203."},{"key":"e_1_3_3_159_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)38134-X"},{"key":"e_1_3_3_160_2","first-page":"252","volume-title":"Proceedings of the Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT\u201904)","author":"Peleska Jan","year":"2004","unstructured":"Jan Peleska, Daniel Gro\u00dfe, Anne E. Haxthausen, and Rolf Drechsler. 2004. Automated verification for train control systems. In Proceedings of the Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT\u201904), E. Schnieder and G. Tarnai (Eds.). Technical University of Braunschweig, Germany, 252\u2013265."},{"key":"e_1_3_3_161_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00551-6"},{"key":"e_1_3_3_162_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-8157-6_61"},{"key":"e_1_3_3_163_2","article-title":"Our model checker PSL up to 60 times faster using AI-tuned proof tactics","year":"2020","unstructured":"Prover. 2020. Our model checker PSL up to 60 times faster using AI-tuned proof tactics. Blog. Retrieved from https:\/\/www.prover.com\/quality\/psl-up-to-sixty-times-faster-using-ai-optimized-proof-strategies\/","journal-title":"Blog"},{"key":"e_1_3_3_164_2","article-title":"Prover Takes Railway Signaling Design Automation to the Next Level with AI and Formal Methods","year":"2024","unstructured":"Prover. 2024. Prover Takes Railway Signaling Design Automation to the Next Level with AI and Formal Methods. News. Retrieved from https:\/\/www.prover.com\/formal-methods\/railway-signaling-design-automation-with-ai-and-formal-methods\/","journal-title":"News"},{"key":"e_1_3_3_165_2","volume-title":"Handbook of Automated Reasoning","author":"Robinson J. Alan","year":"2001","unstructured":"J. Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier, The Netherlands. Retrieved from https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"e_1_3_3_166_2","volume-title":"Formal Methods and the Certification of Critical Systems","author":"Rushby John","year":"1993","unstructured":"John Rushby. 1993. Formal Methods and the Certification of Critical Systems. Technical Report SRI-CSL-93-7. Computer Science Laboratory, SRI International. Retrieved from http:\/\/www.csl.sri.com\/papers\/csl-93-7\/"},{"key":"e_1_3_3_167_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_2"},{"key":"e_1_3_3_168_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_34"},{"key":"e_1_3_3_169_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-77543-8_14"},{"key":"e_1_3_3_170_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19762-8_20"},{"key":"e_1_3_3_171_2","doi-asserted-by":"publisher","DOI":"10.18653\/V1\/2024.NAACL-LONG.81"},{"key":"e_1_3_3_172_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2020.101833"},{"key":"e_1_3_3_173_2","unstructured":"Gunnar St\u00e5lmarck. 1992. A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula. Swedish Patent No. 467 076. International Equivalents: U.S. Patent No. 5 276 897 (1994) European Patent No. 0403 454 (approved 1995)."},{"key":"e_1_3_3_174_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)52173-4"},{"key":"e_1_3_3_175_2","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(90)90127-H"},{"key":"e_1_3_3_176_2","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(93)90091-K"},{"key":"e_1_3_3_177_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00542-2"},{"key":"e_1_3_3_178_2","doi-asserted-by":"publisher","DOI":"10.1155\/2016\/7308604"},{"key":"e_1_3_3_179_2","doi-asserted-by":"publisher","DOI":"10.1109\/MITS.2018.2842230"},{"key":"e_1_3_3_180_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_3_181_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34032-1_24"},{"key":"e_1_3_3_182_2","series-title":"CRPIT","first-page":"309","volume-title":"Proceedings of the 26th Australasian Computer Science Conference (ACSC\u201903)","volume":"16","author":"Winter Kirsten","year":"2003","unstructured":"Kirsten Winter and Neil J. Robinson. 2003. Modelling large railway interlockings and model checking small ones. In Proceedings of the 26th Australasian Computer Science Conference (ACSC\u201903)(CRPIT, Vol. 16), Michael J. Oudshoorn (Ed.). Australian Computer Society, Australia, 309\u2013316. Retrieved from http:\/\/crpit.com\/confpapers\/CRPITV16Winter.pdf"},{"key":"e_1_3_3_183_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_3_184_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-016-0517-1"},{"key":"e_1_3_3_185_2","unstructured":"X2Rail-2. 2018. Deliverable D5.1 Formal Methods (Taxonomy and Survey) Proposed Methods and Applications. Retrieved from https:\/\/projects.shift2rail.org\/download.aspx?id=b4cf6a3d-f1f2-4dd3-ae01-2bada34596b8"},{"key":"e_1_3_3_186_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2016.04.003"},{"key":"e_1_3_3_187_2","doi-asserted-by":"publisher","unstructured":"Ziwei Xu Sanjay Jain and Mohan Kankanhalli. 2024. Hallucination is Inevitable: An Innate Limitation of Large Language Models. arxiv:2401.11817. DOI:10.48550\/arXiv.2401.11817","DOI":"10.48550\/arXiv.2401.11817"},{"key":"e_1_3_3_188_2","doi-asserted-by":"publisher","DOI":"10.52202\/075280-0944"},{"key":"e_1_3_3_189_2","doi-asserted-by":"publisher","DOI":"10.1145\/3783996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3802545","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T11:41:35Z","timestamp":1785238895000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3802545"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,21]]},"references-count":188,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,9,30]]}},"alternative-id":["10.1145\/3802545"],"URL":"https:\/\/doi.org\/10.1145\/3802545","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,21]]},"assertion":[{"value":"2025-08-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-10","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-07-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}