{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T23:53:00Z","timestamp":1770335580916,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319050317","type":"print"},{"value":"9783319050324","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-05032-4_19","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"253-268","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Verification of Solid State Interlocking Programs"],"prefix":"10.1007","author":[{"given":"Phillip","family":"James","sequence":"first","affiliation":[]},{"given":"Andy","family":"Lawrence","sequence":"additional","affiliation":[]},{"given":"Faron","family":"Moller","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]},{"given":"Karim","family":"Kanso","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Chadwick","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"19_CR1","series-title":"LNCS","first-page":"115","volume-title":"ISoLA 2004","author":"PA Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., St\u00e5lmarck, G., \u00c5gren, H., \u00c5kerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115\u2013129. Springer, Heidelberg (2006)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: a declarative language for real-time programming. In: Proceedings of POPL\u201987, pp. 178\u2013188 (1987)","DOI":"10.1145\/41625.41641"},{"issue":"4","key":"19_CR3","first-page":"361","volume":"10","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D.: Formal verification of a railway interlocking system using model checking. FACS 10(4), 361\u2013380 (1998). Springer","journal-title":"FACS"},{"key":"19_CR4","unstructured":"Claessen, K., Sorensson, N.: New techniques that improve mace-style finite model finding. In: Proceedings of CADE\u201903 Workshop: Model Computation (2003)"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Meth. Syst. Des. 19(1), 7\u201334 (2001). Kluwer","journal-title":"Formal Meth. Syst. Des."},{"issue":"4","key":"19_CR6","first-page":"543","volume":"89","author":"N Een","year":"2003","unstructured":"Een, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. ENTCS 89(4), 543\u2013560 (2003)","journal-title":"ENTCS"},{"key":"19_CR7","unstructured":"Fokkink, W., Hollingshead, P.: Verification of interlockings: from control tables to ladder logic diagrams. In: Proceedings of FMICS\u201998, pp. 171\u2013185 (1998)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Groote, J., Koorn, J., Van Vlijmen, S.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Proceedings of Compass\u201995, pp. 57\u201368 (1995)","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"19_CR9","series-title":"SCI","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-01209-9_4","volume-title":"Computer and Information Science 2009","author":"K Han","year":"2009","unstructured":"Han, K., Park, J.: Object-oriented ladder logic development framework based on the unified modeling language. In: Lee, R., Hu, G., Miao, H. (eds.) Computer and Information Science 2009. SCI, vol. 208, pp. 33\u201345. Springer, Heidelberg (2009)"},{"key":"19_CR10","unstructured":"Haxthausen, A.: Automated generation of formal safety conditions from railway interlocking tables. STTT. Springer (to appear)"},{"key":"19_CR11","unstructured":"IEC 61131\u20133 edition 2.0 2003\u201301. International standard. Programmable controllers. Part 3: Programming languages (January 2003)"},{"key":"19_CR12","unstructured":"James, P.: SAT-based model checking and its applications to train control software. MRes Thesis, Swansea University (2010)"},{"key":"19_CR13","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. In: Proceedings of AVoCS\u201910. Electronic Communications of EASST 35 (2010)"},{"key":"19_CR14","unstructured":"Kanso, K.: Formal verification of ladder logic. MRes Thesis, Swansea University (2009)"},{"key":"19_CR15","unstructured":"Kanso, K.: Agda as a platform for the development of verified railway interlocking systems. Ph.D Thesis, Swansea University (2012)"},{"key":"19_CR16","first-page":"19","volume":"250","author":"K Kanso","year":"2009","unstructured":"Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. ENTCS 250, 19\u201331 (2009)","journal-title":"ENTCS"},{"key":"19_CR17","unstructured":"Kanso, K., Setzer, A.: Specifying railway interlocking systems. In: Proceedings of AVoCS\u201909, pp. 233\u2013236 (2009)"},{"key":"19_CR18","unstructured":"Kanso, K., Setzer, A.: Integrating automated and interactive theorem proving in type theory. In: Proceedings of AVoCS\u201910 (2010)"},{"key":"19_CR19","unstructured":"Lawrence, A.: Verification of railway interlockings in SCADE. MRes Thesis, Swansea University (2011)"},{"key":"19_CR20","unstructured":"Lawrence, A., Seisenberger, M.: Verification of railway interlockings in SCADE. In: Proceedings of AVoCS\u201910 (2010)"},{"key":"19_CR21","volume-title":"Railway Control Systems: A Sequel to Railway Signalling","year":"1991","unstructured":"Leach, M. (ed.): Railway Control Systems: A Sequel to Railway Signalling. A & C Black, London (1991)"},{"key":"19_CR22","unstructured":"Minisat. http:\/\/minisat.se"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Rausch, M., Krogh, B.: Formal verification of PLC programs. In: Proceedings of the American Control Conference. IEEE (1998)","DOI":"10.1109\/ACC.1998.694666"},{"key":"19_CR24","unstructured":"St\u00e5lmarck, G.: System for determining propositional logic theorems by applying values and rules to triplets that are generated from boolean formula. US patent: 5,276,897 (1994)"},{"key":"19_CR25","unstructured":"The TPTP problem library for automated theorem proving. http:\/\/www.cs.miami.edu\/tptp\/"},{"key":"19_CR26","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Ina Structures in Constructive Mathematics and Mathematical Logic, Steklov Mathematical Institute (1968)"},{"key":"19_CR27","doi-asserted-by":"crossref","DOI":"10.56021\/9780801839740","volume-title":"What Engineers Know and How They Know It","author":"WG Vincenti","year":"1990","unstructured":"Vincenti, W.G.: What Engineers Know and How They Know It. The Johns Hopkins University Press, Baltimore (1990)"},{"key":"19_CR28","unstructured":"Zoubek, B., Roussel, J.-M., Kwiatkowska, M.: Towards automatic verification of ladder logic programs. In: Proceedings of CESA\u201903. Springer (2003)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05032-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T00:35:58Z","timestamp":1746146158000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}