{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T23:08:53Z","timestamp":1769728133297,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T00:00:00Z","timestamp":1701302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,30]]},"DOI":"10.1145\/3611643.3613874","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:14:38Z","timestamp":1701386078000},"page":"1914-1925","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-0508-6146","authenticated-orcid":false,"given":"Yibo","family":"Dong","sequence":"first","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8125-754X","authenticated-orcid":false,"given":"Xiaoyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8604-2217","authenticated-orcid":false,"given":"Yicong","family":"Xu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1956-3237","authenticated-orcid":false,"given":"Chang","family":"Cai","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5272-6193","authenticated-orcid":false,"given":"Yu","family":"Chen","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2038-439X","authenticated-orcid":false,"given":"Weikai","family":"Miao","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-8285","authenticated-orcid":false,"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9750-8334","authenticated-orcid":false,"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China \/ Shanghai Trusted Industrial Control Platform, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2023,11,30]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"[n. d.]. IC3Ref.. https:\/\/github.com\/arbrad\/IC3ref"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01782772"},{"key":"e_1_3_2_2_3_1","volume-title":"M\u00e9t\u00e9or: A Successful Application of B in a Large Project. In FM\u201999 \u2014 Formal Methods, Jeannette M","author":"Behm Patrick","year":"1999","unstructured":"Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. M\u00e9t\u00e9or: A Successful Application of B in a Large Project. In FM\u201999 \u2014 Formal Methods, Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 369\u2013387. isbn:978-3-540-48119-5"},{"key":"e_1_3_2_2_4_1","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media."},{"key":"e_1_3_2_2_5_1","unstructured":"Armin Biere. 2007. The AIGER and-inverter graph (AIG) format version 20071012."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_3_2_2_7_1","unstructured":"Armin Biere Alessandro Cimatti Edmund M Clarke Ofer Strichman and Yunshan Zhu. [n. d.]. Bounded model checking.. Handbook of satisfiability 185 99 ([n. d.]) 457\u2013481."},{"key":"e_1_3_2_2_8_1","volume-title":"A Case Study","author":"Bonacchi Andrea","unstructured":"Andrea Bonacchi, Alessandro Fantechi, Stefano Bacherini, Matteo Tempestini, and Leonardo Cipriani. 2014. Validation of Railway Interlocking Systems by Formal Verification, A Case Study. In Software Engineering and Formal Methods, Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.). Springer International Publishing, Cham. 237\u2013252. isbn:978-3-319-05032-4"},{"key":"e_1_3_2_2_9_1","volume-title":"Interlocking Design Automation Using Prover Trident","author":"Bor\u00e4lv Arne","unstructured":"Arne Bor\u00e4lv. 2018. Interlocking Design Automation Using Prover Trident. In Formal Methods, Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik de Vink (Eds.). Springer International Publishing, Cham. 653\u2013656. isbn:978-3-319-95582-7"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Simon Busard Quentin Cappart Christophe Limbr\u00e9e Charles Pecheur and Pierre Schaus. 2015. Verification of railway interlocking systems. In ESSS.","DOI":"10.4204\/EPTCS.184.2"},{"key":"e_1_3_2_2_12_1","volume-title":"29th Annual European Simulation and Modelling Conference. 402\u2013409","author":"Cappart Quentin","year":"2015","unstructured":"Quentin Cappart, Christophe Limbr\u00e9e, Pierre Schaus, and Axel Legay. 2015. Verification by discrete simulation of interlocking systems. In 29th Annual European Simulation and Modelling Conference. 402\u2013409."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2017.10"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s40534-016-0119-1"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-19-7510-3_1"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058022"},{"key":"e_1_3_2_2_19_1","volume-title":"Reliability, Safety, and Security of Railway Systems","author":"de Almeida Pereira Dalay Israel","year":"1874","unstructured":"Dalay Israel de Almeida Pereira, David Deharbe, Matthieu Perin, and Philippe Bon. 2019. B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Simon Collart-Dutilleul, Thierry Lecomte, and Alexander Romanovsky (Eds.). Springer International Publishing, Cham. 242\u2013258. isbn:978-3-030-18744-6"},{"key":"e_1_3_2_2_20_1","unstructured":"Niklas E\u00e9n Alan Mishchenko and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD). 125\u2013134."},{"key":"e_1_3_2_2_21_1","volume-title":"International Electrotechnical Commission.","author":"BS EN.","year":"2011","unstructured":"BS EN. 2011. 50128 (2011). Railway Applications-Communication, Signalling and processing systems: Software for railway control and protection systems. International Electrotechnical Commission."},{"key":"e_1_3_2_2_22_1","volume-title":"FORMS\/FORMAT","author":"Ferrari Alessio","year":"2010","unstructured":"Alessio Ferrari, Gianluca Magnani, Daniele Grasso, and Alessandro Fantechi. 2011. Model checking interlocking control tables. In FORMS\/FORMAT 2010. Springer, 107\u2013115."},{"key":"e_1_3_2_2_23_1","volume-title":"Franco Mazzanti, Davide Basile, Alessandro Fantechi, Stefania Gnesi, Andrea Piattino, and Daniele Trentini.","author":"Ferrari Alessio","year":"2019","unstructured":"Alessio Ferrari, Maurice H. ter Beek, Franco Mazzanti, Davide Basile, Alessandro Fantechi, Stefania Gnesi, Andrea Piattino, and Daniele Trentini. 2019. Survey on Formal Methods and Tools in Railways: The ASTRail Approach. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Simon Collart-Dutilleul, Thierry Lecomte, and Alexander Romanovsky (Eds.). Springer International Publishing, Cham. 226\u2013241. isbn:978-3-030-18744-6"},{"key":"e_1_3_2_2_24_1","volume-title":"Vardi","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. AAAI Press."},{"key":"e_1_3_2_2_25_1","volume-title":"Vardi","author":"Giacomo Giuseppe De","year":"2015","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2015. Synthesis for LTL and LDL on finite traces. AAAI Press."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Tim Gonschorek Ludwig Bedau and Frank Ortmeier. 2018. Bringing formal methods on the rail. Safety and Reliability \u2013 Safe Societies in a Changing World.","DOI":"10.1201\/9781351174664-92"},{"key":"e_1_3_2_2_27_1","volume-title":"Applied Bounded Model Checking for Interlocking System Designs","author":"Haxthausen Anne E.","unstructured":"Anne E. Haxthausen, Jan Peleska, and Ralf Pinger. 2014. Applied Bounded Model Checking for Interlocking System Designs. In Software Engineering and Formal Methods, Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.). Springer International Publishing, Cham. 205\u2013220. isbn:978-3-319-05032-4"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_2_29_1","volume-title":"The SafeCap Platform for Modelling Railway Safety and Capacity","author":"Iliasov Alexei","unstructured":"Alexei Iliasov, Ilya Lopatkin, and Alexander Romanovsky. 2013. The SafeCap Platform for Modelling Railway Safety and Capacity. In Computer Safety, Reliability, and Security, Friedemann Bitsch, J\u00e9r\u00e9mie Guiochet, and Mohamed Ka\u00e2niche (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 130\u2013137. isbn:978-3-642-40793-2"},{"key":"e_1_3_2_2_30_1","volume-title":"Formal Verification of Signalling Programs with SafeCap","author":"Iliasov Alexei","unstructured":"Alexei Iliasov, Dominic Taylor, Linas Laibinis, and Alexander Romanovsky. 2018. Formal Verification of Signalling Programs with SafeCap. In Computer Safety, Reliability, and Security, Barbara Gallina, Amund Skavhaug, and Friedemann Bitsch (Eds.). Springer International Publishing, Cham. 91\u2013106. isbn:978-3-319-99130-6"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3141555"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Alexander Ivrii and Arie Gurfinkel. 2015. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD). 65\u201372.","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"e_1_3_2_2_33_1","volume-title":"Verification of Solid State Interlocking Programs","author":"James Phillip","unstructured":"Phillip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso, and Simon Chadwick. 2014. Verification of Solid State Interlocking Programs. In Software Engineering and Formal Methods, Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.). Springer International Publishing, Cham. 253\u2013268. isbn:978-3-319-05032-4"},{"key":"e_1_3_2_2_34_1","volume-title":"Proceedings of the 10th International Workshop on Automated Verification of Critical Systems and the Rodin User and Develop Workshop. Springer, 112\u2013114","author":"Lawrence Andrew","year":"2010","unstructured":"Andrew Lawrence, Monika Seisenberger, Andrew Lawrence, and Monika Seisenberger. 2010. Verification of railway interlockings in scade. In AVOCS\u201910, Proceedings of the 10th International Workshop on Automated Verification of Critical Systems and the Rodin User and Develop Workshop. Springer, 112\u2013114."},{"key":"e_1_3_2_2_35_1","volume-title":"Modelling interlocking systems for railway stations. Master\u2019s thesis","author":"Bliguet Marie Le","unstructured":"Marie Le Bliguet and Andreas Andersen Kj\u00e6 r. 2008. Modelling interlocking systems for railway stations. Master\u2019s thesis. Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_5"},{"key":"e_1_3_2_2_38_1","volume-title":"LTL Satisfiability Checking Revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning (TIME).","author":"Li Jianwen","year":"2013","unstructured":"Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. 2013. LTL Satisfiability Checking Revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning (TIME)."},{"key":"e_1_3_2_2_39_1","volume-title":"SAT-based Explicit LTL Reasoning. Haifa Verification Conference.","author":"Li J.","unstructured":"J. Li, S. Zhu, G. Pu, and M. Vardi. 2015. SAT-based Explicit LTL Reasoning. Haifa Verification Conference."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICICES.2014.7034154"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCCCT49810.2020.9170006"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_2_44_1","volume-title":"In Proceedings of the 7th Workshop on Synthesis.","author":"Michaud T.","unstructured":"T. Michaud and M. Colange. 2018. Reactive synthesis from LTL specification with Spot. In In Proceedings of the 7th Workshop on Synthesis."},{"key":"e_1_3_2_2_45_1","volume-title":"Railml\u2020 a standard data interface for railroad applications. WIT Transactions on The Built Environment, 74","author":"Nash Andrew","year":"2004","unstructured":"Andrew Nash, Daniel Huerlimann, J\u00f6rg Sch\u00fctte, and Vasco Paul Krauss. 2004. Railml\u2020 a standard data interface for railroad applications. WIT Transactions on The Built Environment, 74 (2004)."},{"key":"e_1_3_2_2_46_1","volume-title":"LTL Satisfiability Checking. In International SPIN Workshop on Model Checking of Software.","author":"Kristin","unstructured":"Kristin Y. Rozier and Moshe Y. Vardi. 2007. LTL Satisfiability Checking. In International SPIN Workshop on Model Checking of Software."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_2_2_49_1","volume-title":"Juan Bicarregui, and John S. Fitzgerald.","author":"Woodcock Jim","year":"2009","unstructured":"Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal methods: Practice and experience. ACM Comput. Surv., 41 (2009), 19:1\u201319:36."},{"key":"e_1_3_2_2_50_1","volume-title":"Electronic and Automation Control Conference (IMCEC).","author":"Zhu W.","year":"2021","unstructured":"W. Zhu. 2021. Big Data on Linear Temporal Logic Formulas. In 2021 IEEE 4th Advanced Information Management, Communicates, Electronic and Automation Control Conference (IMCEC)."}],"event":{"name":"ESEC\/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"San Francisco CA USA","acronym":"ESEC\/FSE '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611643.3613874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:10Z","timestamp":1750178230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,30]]},"references-count":50,"alternative-id":["10.1145\/3611643.3613874","10.1145\/3611643"],"URL":"https:\/\/doi.org\/10.1145\/3611643.3613874","relation":{},"subject":[],"published":{"date-parts":[[2023,11,30]]},"assertion":[{"value":"2023-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}