{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:08:21Z","timestamp":1761977301370,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030760"},{"type":"electronic","value":"9783319030777"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03077-7_4","type":"book-chapter","created":{"date-parts":[[2013,10,28]],"date-time":"2013-10-28T01:40:21Z","timestamp":1382924421000},"page":"44-60","source":"Crossref","is-referenced-by-count":13,"title":["Speeding Up the Safety Verification of Programmable Logic Controller Code"],"prefix":"10.1007","author":[{"given":"Tim","family":"Lange","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin R.","family":"Neuh\u00e4u\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Frey, G., Litz, L.: Formal methods in PLC programming. In: Systems, Man, and Cybernetics, vol.\u00a04, pp. 2431\u20132436. IEEE Computer Society (2000)","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"4_CR2","unstructured":"Younis, M.B., Frey, G.: Formalization of existing PLC programs: A survey. In: CESA, pp. 234\u2013239 (2003)"},{"key":"4_CR3","unstructured":"Fokkink, W., Hollingshead, P.: Verification of interlockings: From control tables to ladder logic diagrams. In: FMICS, pp. 171\u2013185 (1998)"},{"issue":"1-2","key":"4_CR4","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J.F. Groote","year":"2000","unstructured":"Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. Journal of Automated Reasoning\u00a024(1-2), 101\u2013125 (2000)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"4_CR5","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\u00a0250(2), 19\u201331 (2009)","journal-title":"ENTCS"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in Instruction List. In: 2000 IEEE Int. Conf. on Systems, Man, and Cybernetics, pp. 2449\u20132454. IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"4_CR7","unstructured":"Meulen, M.: Verification of PLC source code using propositional logic. Master\u2019s thesis, Technical university of Eindhoven (2010)"},{"key":"4_CR8","unstructured":"Pavlovic, O., Pinger, R., Kollmann, M.: Automation of formal verification of PLC programs written in IL. In: Verification Workshop. CEUR Workshop Proceedings, vol.\u00a0259 (2007)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Loeis, K., Younis, M.B., Frey, G.: Application of symbolic and bounded model checking to the verification of logic control systems. In: ETFA, pp. 247\u2013250 (2005)","DOI":"10.1109\/ETFA.2005.1612527"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Pavlovic, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: ICST, pp. 439\u2013448 (2010)","DOI":"10.1109\/ICST.2010.10"},{"key":"4_CR11","unstructured":"S\u00fclflow, A., Drechsler, R.: Verification of PLC programs using formal proof techniques. In: FORMS\/FORMAT, pp. 43\u201350 (2008)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24690-6_6","volume-title":"Software Engineering and Formal Methods","author":"J.O. Blech","year":"2011","unstructured":"Blech, J.O., Biha, S.O.: Verification of PLC properties based on formal semantics in Coq. In: SEFM. Volume 7041 of LNCS., Springer (2011) 58\u201373"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD 2009, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"John, K., Tiegelkamp, M.: IEC 61131-3: Programming Industrial Automation Systems. Springer (2010)","DOI":"10.1007\/978-3-642-12015-2"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"4_CR16","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann (1997)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173\u2013180. IEEE (2007)","DOI":"10.1109\/FMCAD.2007.4401997"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03077-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T18:28:53Z","timestamp":1746037733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03077-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030760","9783319030777"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03077-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}