{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T10:20:04Z","timestamp":1783160404270,"version":"3.54.6"},"reference-count":84,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,5,28]],"date-time":"2026-05-28T00:00:00Z","timestamp":1779926400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["PE00000014"],"award-info":[{"award-number":["PE00000014"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["2022Z4N84X_001 CUP J53C24002800006"],"award-info":[{"award-number":["2022Z4N84X_001 CUP J53C24002800006"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["EDIT4MCC"],"award-info":[{"award-number":["EDIT4MCC"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100009879","name":"Regione Emilia-Romagna","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100009879","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100022612","name":"Ministero della Difesa","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100022612","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100024370","name":"Governo Italiano Ministero dell&apos;Istruzione e del Merito","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100024370","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computers &amp; Security"],"published-print":{"date-parts":[[2026,10]]},"DOI":"10.1016\/j.cose.2026.104983","type":"journal-article","created":{"date-parts":[[2026,5,28]],"date-time":"2026-05-28T07:00:58Z","timestamp":1779951658000},"page":"104983","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["PLC-Defuser: Detecting hidden Ladder Logic Bombs in PLCs via Control Flow Graph and model checking"],"prefix":"10.1016","volume":"169","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1767-7256","authenticated-orcid":false,"given":"Lorenzo","family":"Rinieri","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2064-8261","authenticated-orcid":false,"given":"Antonio","family":"Iacobelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0101-2551","authenticated-orcid":false,"given":"Andrea","family":"Melis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3962-5513","authenticated-orcid":false,"given":"Marco","family":"Prandini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6669-8072","authenticated-orcid":false,"given":"Franco","family":"Callegati","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.cose.2026.104983_b1","unstructured":"Abbas, S.G., Ozmen, M.O., Alsaheel, A., Khan, A., Celik, Z.B., Xu, D., 2024. {SAIN}: Improving {ICS} Attack Detection Sensitivity via {State-Aware} Invariants. In: 33rd USENIX Security Symposium (USENIX Security 24). pp. 6597\u20136613."},{"key":"10.1016\/j.cose.2026.104983_b2","series-title":"Compilers: principles, techniques, and tools","author":"Alfred","year":"2007"},{"issue":"7","key":"10.1016\/j.cose.2026.104983_b3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/390013.808479","article-title":"Control flow analysis","volume":"5","author":"Allen","year":"1970","journal-title":"ACM Sigplan Not."},{"issue":"4","key":"10.1016\/j.cose.2026.104983_b4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/j.cose.2026.104983_b5","series-title":"IECON 2021\u201347th Annual Conference of the IEEE Industrial Electronics Society","first-page":"1","article-title":"A control injection attack against S7 PLCs-manipulating the decompiled code","author":"Alsabbagh","year":"2021"},{"key":"10.1016\/j.cose.2026.104983_b6","series-title":"2021 22nd IEEE International Conference on Industrial Technology","first-page":"986","article-title":"A stealth program injection attack against S7-300 PLCs","volume":"1","author":"Alsabbagh","year":"2021"},{"issue":"4","key":"10.1016\/j.cose.2026.104983_b7","doi-asserted-by":"crossref","first-page":"596","DOI":"10.3390\/automation3040030","article-title":"A flashback on control logic injection attacks against programmable logic controllers","volume":"3","author":"Alsabbagh","year":"2022","journal-title":"Automation"},{"key":"10.1016\/j.cose.2026.104983_b8","series-title":"Real-Time: Theory in Practice: REX Workshop Mook, the Netherlands, June 3\u20137, 1991 Proceedings","first-page":"74","article-title":"Logics and models of real time: A survey","author":"Alur","year":"1992"},{"key":"10.1016\/j.cose.2026.104983_b9","series-title":"IEEE Global Humanitarian Technology Conference (GHTC 2014)","first-page":"585","article-title":"OpenPLC: An open source alternative to automation","author":"Alves","year":"2014"},{"key":"10.1016\/j.cose.2026.104983_b10","series-title":"2013 IEEE 18th Conference on Emerging Technologies & Factory Automation","first-page":"1","article-title":"Points-to analysis of IEC 61131-3 programs: Implementation and application","author":"Angerer","year":"2013"},{"key":"10.1016\/j.cose.2026.104983_b11","series-title":"2024 IEEE International Symposium on Hardware Oriented Security and Trust","first-page":"182","article-title":"Charlie, charlie, charlie on industrial control systems: PLC control logic attacks by design, not by chance","author":"Ayub","year":"2024"},{"key":"10.1016\/j.cose.2026.104983_b12","series-title":"2021 IEEE Security and Privacy Workshops","first-page":"383","article-title":"Empirical study of PLC authentication protocols in industrial control systems","author":"Ayub","year":"2021"},{"key":"10.1016\/j.cose.2026.104983_b13","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/j.cose.2026.104983_b14","series-title":"Integration of Software Specification Techniques for Applications in Engineering: Priority Program SoftSpez of the German Research Foundation (DFG), Final Report","first-page":"517","article-title":"Verification of PLC programs given as sequential function charts","author":"Bauer","year":"2004"},{"issue":"3","key":"10.1016\/j.cose.2026.104983_b15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.3390\/fi15030095","article-title":"When operation technology meets information technology: challenges and opportunities","volume":"15","author":"Berardi","year":"2023","journal-title":"Futur. Internet"},{"key":"10.1016\/j.cose.2026.104983_b16","series-title":"Verification of programmable logic controller code using model checking and static analysis","author":"Biallas","year":"2016"},{"key":"10.1016\/j.cose.2026.104983_b17","doi-asserted-by":"crossref","unstructured":"Biallas, S., Brauer, J., Kowalewski, S., 2012. Arcade. PLC: A verification platform for programmable logic controllers. In: Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering. pp. 338\u2013341.","DOI":"10.1145\/2351676.2351741"},{"key":"10.1016\/j.cose.2026.104983_b18","series-title":"2011 IEEE 35th Annual Computer Software and Applications Conference","first-page":"118","article-title":"A formal semantics of PLC programs in coq","author":"Biha","year":"2011"},{"key":"10.1016\/j.cose.2026.104983_b19","series-title":"NOMS 2018-2018 IEEE\/IFIP Network Operations and Management Symposium","first-page":"1","article-title":"Kathar\u00e1: A container-based framework for implementing network function virtualization and software defined networks","author":"Bonofiglio","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b20","article-title":"Intrepid: An SMT-based model checker for control engineering and industrial automation","volume":"vol. 8","author":"Bruttomesso","year":"2019"},{"key":"10.1016\/j.cose.2026.104983_b21","series-title":"Rockwell PLC Logic Analysis Using Model Checking","author":"Bruttomesso","year":"2022"},{"key":"10.1016\/j.cose.2026.104983_b22","doi-asserted-by":"crossref","unstructured":"Bytes, A., Rajput, P.H.N., Doumanidis, C., Maniatakos, M., Zhou, J., Tippenhauer, N.O., 2023. Fieldfuzz: In situ blackbox fuzzing of proprietary industrial automation runtimes via the network. In: Proceedings of the 26th International Symposium on Research in Attacks, Intrusions and Defenses. pp. 499\u2013512.","DOI":"10.1145\/3607199.3607226"},{"key":"10.1016\/j.cose.2026.104983_b23","first-page":"2449","article-title":"Towards the automatic verification of PLC programs written in Instruction List","volume":"vol. 4","author":"Canet","year":"2000"},{"key":"10.1016\/j.cose.2026.104983_b24","doi-asserted-by":"crossref","unstructured":"Castellanos, J.H., Ochoa, M., Cardenas, A.A., Arden, O., Zhou, J., 2021. AttkFinder: Discovering attack vectors in PLC programs using information flow analysis. In: Proceedings of the 24th International Symposium on Research in Attacks, Intrusions and Defenses. pp. 235\u2013250.","DOI":"10.1145\/3471621.3471864"},{"key":"10.1016\/j.cose.2026.104983_b25","series-title":"2018 International Conference on Intelligent Rail Transportation","first-page":"1","article-title":"Formal methods for industrial interlocking verification","author":"Chadwick","year":"2018"},{"issue":"3","key":"10.1016\/j.cose.2026.104983_b26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1541880.1541882","article-title":"Anomaly detection: A survey","volume":"41","author":"Chandola","year":"2009","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.cose.2026.104983_b27","article-title":"Constructing PLC binary program model for detection purposes","volume":"vol. 1087","author":"Chang","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b28","series-title":"International Conference on Cloud Computing and Security","first-page":"241","article-title":"Detecting PLC program malicious behaviors based on state verification","author":"Chang","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b29","series-title":"2018 IEEE Symposium on Security and Privacy","first-page":"648","article-title":"Learning from mutants: Using code mutation to learn and monitor invariants of a cyber-physical system","author":"Chen","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b30","volume":"vol. 10","author":"Clarke","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b31","series-title":"LASER Summer School on Software Engineering","first-page":"1","article-title":"Model checking and the state explosion problem","author":"Clarke","year":"2011"},{"key":"10.1016\/j.cose.2026.104983_b32","series-title":"International Conference on Accelerator and Large Experimental Physics Control Systems","article-title":"PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques","author":"Darvas","year":"2015"},{"key":"10.1016\/j.cose.2026.104983_b33","first-page":"284","article-title":"Formal verification of complex properties on PLC programs","author":"Darvas","year":"2014"},{"key":"10.1016\/j.cose.2026.104983_b34","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de Moura","year":"2008"},{"key":"10.1016\/j.cose.2026.104983_b35","first-page":"8","article-title":"Safe programming of PLC using formal verification methods","volume":"7","author":"De Smet","year":"2000","journal-title":"Comput. Sci."},{"key":"10.1016\/j.cose.2026.104983_b36","first-page":"1","article-title":"TRITON: The first ICS cyber attack on safety instrument systems","volume":"2018","author":"Di Pinto","year":"2018","journal-title":"Proc. Black Hat USA"},{"issue":"6","key":"10.1016\/j.cose.2026.104983_b37","first-page":"29","article-title":"W32. stuxnet dossier","volume":"5","author":"Falliere","year":"2011","journal-title":"White Pap. Symantec Corp. Secur. Response"},{"key":"10.1016\/j.cose.2026.104983_b38","series-title":"ETFA2011","first-page":"1","article-title":"A model-driven engineering approach to formal verification of PLC programs","author":"Farines","year":"2011"},{"key":"10.1016\/j.cose.2026.104983_b39","series-title":"NDSS","first-page":"1","article-title":"A Systematic Framework to Generate Invariants for Anomaly Detection in Industrial Control Systems.","author":"Feng","year":"2019"},{"issue":"6","key":"10.1016\/j.cose.2026.104983_b40","doi-asserted-by":"crossref","first-page":"1400","DOI":"10.1109\/TII.2015.2489184","article-title":"Applying model checking to industrial-sized PLC programs","volume":"11","author":"Fern\u00e1ndez Adiego","year":"2015","journal-title":"IEEE Trans. Ind. Inform."},{"key":"10.1016\/j.cose.2026.104983_b41","unstructured":"Finck, C., Dohrmann, T., 2023. A Decade After Stuxnet: How Siemens S7 is Still an Attacker\u2019s Heaven."},{"key":"10.1016\/j.cose.2026.104983_b42","series-title":"NASA Formal Methods Symposium","first-page":"427","article-title":"Verifying PLC programs via monitors: Extending the integration of fret and plcverif","author":"Fink","year":"2024"},{"key":"10.1016\/j.cose.2026.104983_b43","series-title":"2006 8th International Workshop on Discrete Event Systems","first-page":"182","article-title":"Efficient representation for formal verification of PLC programs","author":"Gourcuff","year":"2006"},{"key":"10.1016\/j.cose.2026.104983_b44","series-title":"Computer Security","first-page":"110","article-title":"On Ladder Logic Bombs in Industrial Control Systems","author":"Govil","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b45","doi-asserted-by":"crossref","unstructured":"Grandgenett, R., Mahoney, W., Gandhi, R., 2015. Authentication bypass and remote escalated I\/O command attacks. In: Proceedings of the 10th Annual Cyber and Information Security Research Conference. pp. 1\u20137.","DOI":"10.1145\/2746266.2746268"},{"key":"10.1016\/j.cose.2026.104983_b46","doi-asserted-by":"crossref","unstructured":"Guo, S., Wu, M., Wang, C., 2017. Symbolic execution of programmable logic controller code. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. pp. 326\u2013336.","DOI":"10.1145\/3106237.3106245"},{"key":"10.1016\/j.cose.2026.104983_b47","series-title":"2021 28th Asia-Pacific Software Engineering Conference","first-page":"152","article-title":"Data Flow Testing for PLC Programs via Dynamic Symbolic Execution","author":"He","year":"2021"},{"key":"10.1016\/j.cose.2026.104983_b48","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2021.102608","article-title":"Automated test generation for IEC 61131-3 ST programs via dynamic symbolic execution","volume":"206","author":"He","year":"2021","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.cose.2026.104983_b49","series-title":"History of Industrial Control System Cyber Incidents","author":"Hemsley","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b50","doi-asserted-by":"crossref","DOI":"10.1016\/j.ijcip.2021.100470","article-title":"Vulnerability analysis of S7 PLCs: Manipulating the security mechanism","volume":"35","author":"Hui","year":"2021","journal-title":"Int. J. Crit. Infrastruct. Prot."},{"key":"10.1016\/j.cose.2026.104983_b51","series-title":"2024 IEEE 7th International Conference on Industrial Cyber-Physical Systems","first-page":"1","article-title":"Detection of ladder logic bombs in PLC control programs: an architecture based on formal verification","author":"Iacobelli","year":"2024"},{"key":"10.1016\/j.cose.2026.104983_b52","series-title":"Programmable Controllers - Part 3: Programming Languages","author":"I.E.C. technical committee","year":"2013"},{"key":"10.1016\/j.cose.2026.104983_b53","series-title":"Programmable controllers \u2013 Part 10: PLC open XML exchange format, v1.0","author":"International Electrotechnical Commission","year":"2019"},{"key":"10.1016\/j.cose.2026.104983_b54","series-title":"Binary Analysis Research (BAR) Workshop, Network and Distributed System Security Symposium","first-page":"1","article-title":"CLIK on plcs! attacking control logic with decompilation and virtual PLC","author":"Kalle","year":"2019"},{"key":"10.1016\/j.cose.2026.104983_b55","series-title":"SoutheastCon 2017","first-page":"1","article-title":"Formal verification of ladder logic programs using NuSMV","author":"Kottler","year":"2017"},{"issue":"2","key":"10.1016\/j.cose.2026.104983_b56","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"10.1016\/j.cose.2026.104983_b57","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/PL00008921","article-title":"Fairness and hyperfairness","volume":"13","author":"Lamport","year":"2000","journal-title":"Distrib. Comput."},{"issue":"1","key":"10.1016\/j.cose.2026.104983_b58","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3546579","article-title":"Industrial control systems security via runtime enforcement","volume":"26","author":"Lanotte","year":"2022","journal-title":"ACM Trans. Priv. Secur."},{"issue":"62","key":"10.1016\/j.cose.2026.104983_b59","first-page":"1","article-title":"German steel mill cyber attack","volume":"30","author":"Lee","year":"2014","journal-title":"Ind. Control. Syst."},{"key":"10.1016\/j.cose.2026.104983_b60","unstructured":"L\u00f3pez-Morales, E., Planta, U., Rubio-Medrano, C., Abbasi, A., Cardenas, A.A., 2024. {SoK}: Security of Programmable Logic Controllers. In: 33rd USENIX Security Symposium (USENIX Security 24). pp. 7103\u20137122."},{"key":"10.1016\/j.cose.2026.104983_b61","series-title":"2016 International Workshop on Cyber-Physical Systems for Smart Water Networks (CySWater)","first-page":"31","article-title":"SWaT: A water treatment testbed for research and training on ICS security","author":"Mathur","year":"2016"},{"key":"10.1016\/j.cose.2026.104983_b62","series-title":"NDSS","article-title":"A trusted safety verifier for process controller code.","volume":"14","author":"McLaughlin","year":"2014"},{"key":"10.1016\/j.cose.2026.104983_b63","doi-asserted-by":"crossref","DOI":"10.1016\/j.ijcip.2021.100464","article-title":"Looking back to look forward: Lessons learnt from cyber-attacks on industrial control systems","volume":"35","author":"Miller","year":"2021","journal-title":"Int. J. Crit. Infrastruct. Prot."},{"issue":"2","key":"10.1016\/j.cose.2026.104983_b64","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1109\/37.272781","article-title":"Modeling programmable logic controllers for logic verification","volume":"14","author":"Moon","year":"1994","journal-title":"IEEE Control Syst. Mag."},{"key":"10.1016\/j.cose.2026.104983_b65","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10817-017-9415-7","article-title":"Translation of IEC 61131-3 function block diagrams to PVS for formal verification with real-time nuclear application","volume":"60","author":"Newell","year":"2018","journal-title":"J. Automat. Reason."},{"key":"10.1016\/j.cose.2026.104983_b66","unstructured":"Pavlovic, O., Pinger, R., Kollmann, M., 2007. Automated formal verification of PLC programs written in IL. In: Conference on Automated Deduction. CADE, pp. 152\u2013163."},{"key":"10.1016\/j.cose.2026.104983_b67","doi-asserted-by":"crossref","unstructured":"Pickren, R., Shekari, T., Zonouz, S., Beyah, R., 2024. Compromising industrial processes using web-based programmable logic controller malware. In: Network and Distributed System Security (NDSS) Symposium.","DOI":"10.14722\/ndss.2024.23049"},{"key":"10.1016\/j.cose.2026.104983_b68","series-title":"Plcopen logic certification","author":"PLCopen","year":"2018"},{"issue":"1","key":"10.1016\/j.cose.2026.104983_b69","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/TII.2016.2604760","article-title":"Static code analysis of IEC 61131-3 programs: Comprehensive tool support and experiences from large-scale industrial application","volume":"13","author":"Pr\u00e4hofer","year":"2016","journal-title":"IEEE Trans. Ind. Informatics"},{"issue":"7","key":"10.1016\/j.cose.2026.104983_b70","first-page":"pp","article-title":"Safety properties verification of ladder diagram programs","volume":"36","author":"Roussel","year":"2002","journal-title":"J. Eur. Des Syst. Automatis\u00e9s (JESA)"},{"key":"10.1016\/j.cose.2026.104983_b71","series-title":"2024 IEEE Symposium on Security and Privacy","first-page":"312","article-title":"A tale of two Industroyers: It was the season of darkness","author":"Salazar","year":"2024"},{"key":"10.1016\/j.cose.2026.104983_b72","series-title":"2018 International Conference on Computer and Applications","first-page":"348","article-title":"PLC code-level vulnerabilities","author":"Serhane","year":"2018"},{"key":"10.1016\/j.cose.2026.104983_b73","series-title":"Proceedings of the 2014 IEEE Emerging Technology and Factory Automation","first-page":"1","article-title":"Applying static code analysis on industrial controller code","author":"Stattelmann","year":"2014"},{"key":"10.1016\/j.cose.2026.104983_b74","series-title":"2021 IEEE European Symposium on Security and Privacy (EuroS&P)","first-page":"385","article-title":"SoK: Attacks on industrial control logic and formal verification-based defenses","author":"Sun","year":"2021"},{"key":"10.1016\/j.cose.2026.104983_b75","unstructured":"Tychalas, D., Benkraouda, H., Maniatakos, M., 2021. {ICSFuzz}: Manipulating {I\/Os} and repurposing binary code to enable instrumented fuzzing in {ICS} control applications. In: 30th USENIX Security Symposium (USENIX Security 21). pp. 2847\u20132862."},{"key":"10.1016\/j.cose.2026.104983_b76","doi-asserted-by":"crossref","unstructured":"Ukegbu, C., Mehrpouyan, H., 2023. Benchmarks for the Verification of Safety and Security Properties of PLC Programs in Cooperative Verification Environments. In: Proceedings of the 2023 8th International Conference on Information Systems Engineering. pp. 19\u201328.","DOI":"10.1145\/3641032.3641046"},{"key":"10.1016\/j.cose.2026.104983_b77","series-title":"2022 International Conference on Electronic Systems and Intelligent Computing","article-title":"Towards Quantum Artificial Intelligence Electromagnetic Prediction Models for Ladder Logic Bombs and Faults in Programmable Logic Controllers","author":"Vaidyan","year":"2022"},{"issue":"2","key":"10.1016\/j.cose.2026.104983_b78","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1080\/23742917.2023.2171538","article-title":"A digital twin internal to a PLC to detect malicious commands and ladder logic that potentially cause safety violations","volume":"7","author":"Werth","year":"2023","journal-title":"J. Cyber Secur. Technol."},{"issue":"2\u20133","key":"10.1016\/j.cose.2026.104983_b79","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0166-3615(94)90017-5","article-title":"The purdue enterprise reference architecture","volume":"24","author":"Williams","year":"1994","journal-title":"Comput. Ind."},{"issue":"16","key":"10.1016\/j.cose.2026.104983_b80","doi-asserted-by":"crossref","DOI":"10.1002\/cpe.5724","article-title":"A malware detection method using satisfiability modulo theory model checking for the programmable logic controller system","volume":"34","author":"Xie","year":"2022","journal-title":"Concurr. Comput.: Pr. Exp."},{"key":"10.1016\/j.cose.2026.104983_b81","series-title":"ICT Systems Security and Privacy Protection: 34th IFIP TC 11 International Conference, SEC 2019, Lisbon, Portugal, June 25-27, 2019, Proceedings 34","first-page":"33","article-title":"Control logic injection attacks on industrial control systems","author":"Yoo","year":"2019"},{"key":"10.1016\/j.cose.2026.104983_b82","series-title":"Detection of Intrusions and Malware, and Vulnerability Assessment: 16th International Conference, DIMVA 2019, Gothenburg, Sweden, June 19\u201320, 2019, Proceedings 16","first-page":"109","article-title":"Overshadow plc to detect remote control-logic injection attacks","author":"Yoo","year":"2019"},{"key":"10.1016\/j.cose.2026.104983_b83","series-title":"2019 IEEE Symposium on Security and Privacy","first-page":"522","article-title":"Towards automated safety vetting of plc code in real-world plants","author":"Zhang","year":"2019"},{"issue":"1","key":"10.1016\/j.cose.2026.104983_b84","article-title":"Formal verification of ST programs using CSP","volume":"2010","author":"Zhou","year":"2021","journal-title":"J. Phys.: Conf. Ser."}],"container-title":["Computers &amp; Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167404826001598?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167404826001598?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T10:11:50Z","timestamp":1783159910000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167404826001598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,10]]},"references-count":84,"alternative-id":["S0167404826001598"],"URL":"https:\/\/doi.org\/10.1016\/j.cose.2026.104983","relation":{},"ISSN":["0167-4048"],"issn-type":[{"value":"0167-4048","type":"print"}],"subject":[],"published":{"date-parts":[[2026,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"PLC-Defuser: Detecting hidden Ladder Logic Bombs in PLCs via Control Flow Graph and model checking","name":"articletitle","label":"Article Title"},{"value":"Computers & Security","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cose.2026.104983","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Ltd.","name":"copyright","label":"Copyright"}],"article-number":"104983"}}