{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,22]],"date-time":"2026-10-22T00:08:00Z","timestamp":1792627680835,"version":"4.5.0"},"reference-count":23,"publisher":"IEEE","license":[{"start":{"date-parts":[[2024,5,12]],"date-time":"2024-05-12T00:00:00Z","timestamp":1715472000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,5,12]],"date-time":"2024-05-12T00:00:00Z","timestamp":1715472000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,5,12]]},"DOI":"10.1109\/icps59941.2024.10639995","type":"proceedings-article","created":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T17:24:30Z","timestamp":1724693070000},"page":"1-7","source":"Crossref","is-referenced-by-count":5,"title":["Detection of Ladder Logic Bombs in PLC Control Programs: an Architecture based on Formal Verification"],"prefix":"10.1109","author":[{"given":"Antonio","family":"Iacobelli","sequence":"first","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lorenzo","family":"Rinieri","sequence":"additional","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Melis","sequence":"additional","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir Al","family":"Sadi","sequence":"additional","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Prandini","sequence":"additional","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Franco","family":"Callegati","sequence":"additional","affiliation":[{"name":"Università di Bologna,Department of Computer Science and Engineering,Bologna,Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2021.3094360"},{"key":"ref2","year":"2013","journal-title":"Programmable controllers - Part 3: Programming languages"},{"key":"ref3","article-title":"WIN32\/INDUSTROYER: A new threat for industrial control systems","author":"Cherepanov","year":"2017","journal-title":"White paper"},{"key":"ref4","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"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2011.67"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SECON.2017.7925390"},{"key":"ref7","first-page":"8","article-title":"Safe programming of PLC using formal verification methods","volume":"7","author":"De Smet","year":"2000","journal-title":"Computer Science"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2011.6034994"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/37.272781"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2011.6058983"},{"key":"ref11","article-title":"UniboSecurityResearch\/PLC-LD-dataset: v1.0.0","author":"Iacobelli","year":"2023"},{"key":"ref12","article-title":"Intrepid: An SMT-based model checker for control engineering and industrial automation","volume-title":"SMT Workshop","volume":"8","author":"Bruttomesso"},{"key":"ref13","article-title":"XML formats for IEC 61131-3, v2.01","author":"Committee","year":"2009"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/GHTC.2014.6970342"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ICESIC53714.2022.9783543"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72817-9_8"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1088\/1742-6596\/2010\/1\/012072"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"ref20","article-title":"Plcopen logic certification","year":"2018"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1080\/23742917.2023.2171538"},{"key":"ref22","article-title":"Rockwell PLC Logic Analysis Using Model Checking","author":"Bruttomesso","year":"2022"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3471621.3471864"}],"event":{"name":"2024 IEEE 7th International Conference on Industrial Cyber-Physical Systems (ICPS)","location":"St. Louis, MO, USA","start":{"date-parts":[[2024,5,12]]},"end":{"date-parts":[[2024,5,15]]}},"container-title":["2024 IEEE 7th International Conference on Industrial Cyber-Physical Systems (ICPS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10639954\/10639940\/10639995.pdf?arnumber=10639995","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,2]],"date-time":"2024-09-02T04:47:44Z","timestamp":1725252464000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10639995\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,12]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/icps59941.2024.10639995","relation":{},"subject":[],"published":{"date-parts":[[2024,5,12]]}}}