{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:58Z","timestamp":1748664658731,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319247038"},{"type":"electronic","value":"9783319247045"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24704-5_15","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T05:31:29Z","timestamp":1443072689000},"page":"241-256","source":"Crossref","is-referenced-by-count":3,"title":["Towards Interactive Verification of Programmable Logic Controllers Using Modal Kleene Algebra and KIV"],"prefix":"10.1007","author":[{"given":"Roland","family":"Gl\u00fcck","sequence":"first","affiliation":[]},{"given":"Florian Benedikt","family":"Krebs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"15_CR1","unstructured":"Coq. https:\/\/coq.inria.fr\/ (Online; accessed July 7, 2015)"},{"key":"15_CR2","unstructured":"IEC61131. http:\/\/webstore.iec.ch\/webstore\/webstore.nsf\/artnum\/048541opendocument (Online; accessed April 1, 2015)"},{"key":"15_CR3","unstructured":"Isabelle. https:\/\/isabelle.in.tum.de\/ (Online; accessed July 7, 2015)"},{"key":"15_CR4","unstructured":"The KIV system. http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv\/ (Online; accessed November 5, 2014)"},{"key":"15_CR5","unstructured":"NuSMV. http:\/\/nusmv.fbk.eu\/ (Online; accessed July 7, 2015)"},{"key":"15_CR6","unstructured":"Prover9. https:\/\/www.cs.unm.edu\/~mccune\/mace4\/ (Online; accessed July 7, 2015)"},{"key":"15_CR7","unstructured":"Step7. http:\/\/w3.siemens.com\/mcms\/simatic-controller-software\/en\/step7\/ (Online; accessed April 1, 2015)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"A. Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on kleene algebra in isabelle\/hol. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 197\u2013212. Springer, Heidelberg (2013)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 363\u2013366. Springer, Heidelberg (2000)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-06251-8_11","volume-title":"Relational and Algebraic Methods in Computer Science","author":"R. Berghammer","year":"2014","unstructured":"Berghammer, R., H\u00f6fner, P., Stucke, I.: Automated verification of relational while-programs. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) RAMiCS 2014. LNCS, vol.\u00a08428, pp. 173\u2013190. Springer, Heidelberg (2014)"},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1109\/TII.2011.2182653","volume":"8","author":"H. Carlsson","year":"2012","unstructured":"Carlsson, H., Svensson, B., Danielson, F., Lennartson, B.: Methods for reliable simulation-based PLC code verification. IEEE Trans. Industrial Informatics\u00a08(2), 267\u2013278 (2012)","journal-title":"IEEE Trans. Industrial Informatics"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Dang, H., H\u00f6fner, P.: Automated higher-order reasoning about quantales. In: Schmidt, R.A., Schulz, S., Konev, B. (eds.) Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR 2010. EPiC Series, vol.\u00a09, pp. 40\u201351. EasyChair, Edinburgh (2010)","DOI":"10.29007\/l2sz"},{"key":"15_CR13","first-page":"93","volume":"1","author":"J. Desharnais","year":"2004","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Modal kleene algebra and applications - a survey. Journal on Relational Methods in Computer Science\u00a01, 93\u2013131 (2004)","journal-title":"Journal on Relational Methods in Computer Science"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic\u00a07, 798\u2013833 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-78913-0_15","volume-title":"Relations and Kleene Algebra in Computer Science","author":"P. H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P.: Automated reasoning for hybrid systems - two case studies -. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS\/AKA 2008. LNCS, vol.\u00a04988, pp. 191\u2013205. Springer, Heidelberg (2008)"},{"key":"15_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"issue":"7","key":"15_CR17","doi-asserted-by":"publisher","first-page":"1131","DOI":"10.1016\/j.infsof.2009.01.003","volume":"51","author":"E. Jee","year":"2009","unstructured":"Jee, E., Yoo, J., Cha, S.D., Bae, D.: A data flow-based structural testing technique for FBD programs. Information & Software Technology\u00a051(7), 1131\u20131139 (2009)","journal-title":"Information & Software Technology"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390","DOI":"10.1006\/inco.1994.1037"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/11784180_21","volume-title":"Algebraic Methodology and Software Technology","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., H\u00f6fner, P., Struth, G.: Quantales and temporal logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 263\u2013277. Springer, Heidelberg (2006)"},{"issue":"3","key":"15_CR20","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0951-8320(03)00090-5","volume":"81","author":"F. Ortmeier","year":"2003","unstructured":"Ortmeier, F., Schellhorn, G., Thums, A., Reif, W., Hering, B., Trappschuh, H.: Safety analysis of the height control system for the elbtunnel. Rel. Eng. & Sys. Safety\u00a081(3), 259\u2013268 (2003)","journal-title":"Rel. Eng. & Sys. Safety"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Pavlovic, O., Ehrich, H.: Model checking PLC software written in function block diagram. In: Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, April 7-9. CEUR Workshop Proceedings. IEEE Computer Society (2010)","DOI":"10.1109\/ICST.2010.10"},{"key":"15_CR22","unstructured":"Pavlovic, O., Pinger, R., Kollmann, M.: Automation of formal verification of PLC programs written in IL. In: Beckert, B. (ed.) Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16. CEUR Workshop Proceedings, vol.\u00a0259. CEUR-WS.org (2007)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11813040_3","volume-title":"FM 2006: Formal Methods","author":"J. Schmitt","year":"2006","unstructured":"Schmitt, J., Hoffmann, A., Balser, M., Reif, W., Marcos, M.: Interactive verification of medical guidelines. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 32\u201347. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24704-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T19:52:52Z","timestamp":1748634772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24704-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319247038","9783319247045"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24704-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}