{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:06:10Z","timestamp":1760731570251,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T00:00:00Z","timestamp":1669680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["2021R1A5A1021944"],"award-info":[{"award-number":["2021R1A5A1021944"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Institute of Information & communications Technology Planning & Evaluation","award":["2022-0-00103"],"award-info":[{"award-number":["2022-0-00103"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,11,29]]},"DOI":"10.1145\/3563822.3568016","type":"proceedings-article","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T21:17:50Z","timestamp":1669929470000},"page":"56-67","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT"],"prefix":"10.1145","author":[{"given":"Jaeseo","family":"Lee","sequence":"first","affiliation":[{"name":"POSTECH, South Korea"}]},{"given":"Sangki","family":"Kim","sequence":"additional","affiliation":[{"name":"POSTECH, South Korea"}]},{"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[{"name":"POSTECH, South Korea"}]}],"member":"320","published-online":{"date-parts":[[2022,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00033"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2013.81"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68034-7_5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.03.006"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27863-4_28"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351741"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167132.3167334"},{"volume-title":"Advances in Computing, Andr\u00e9s Solano and Hugo Ordo\u00f1ez (Eds.)","author":"Cadavid H\u00e9ctor","key":"e_1_3_2_1_9_1","unstructured":"H\u00e9ctor Cadavid , Alexander P\u00e9rez , and Camilo Rocha . 2017. Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots . In Advances in Computing, Andr\u00e9s Solano and Hugo Ordo\u00f1ez (Eds.) . Springer International Publishing , Cham . 611\u2013626. isbn:978-3-319-66562-7 H\u00e9ctor Cadavid, Alexander P\u00e9rez, and Camilo Rocha. 2017. Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots. In Advances in Computing, Andr\u00e9s Solano and Hugo Ordo\u00f1ez (Eds.). Springer International Publishing, Cham. 611\u2013626. isbn:978-3-319-66562-7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_1_12_1","unstructured":"M. Clavel F. Dur\u00e1n S. Eker J. Meseguer P. Lincoln N. Mart\u00ed-Oliet and C. Talcott. 2007. All About Maude \u2013 A High-Performance Logical Framework (Lecture Notes in Computer Science Vol. 4350). Springer Berlin Heidelberg. \t\t\t\t  M. Clavel F. Dur\u00e1n S. Eker J. Meseguer P. Lincoln N. Mart\u00ed-Oliet and C. Talcott. 2007. All About Maude \u2013 A High-Performance Logical Framework (Lecture Notes in Computer Science Vol. 4350). Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_13_1","first-page":"61131","article-title":"Programmable controllers-part 3: Programming languages","author":"International Electrotechnical Commission","year":"1993","unstructured":"International Electrotechnical Commission . 1993 . Programmable controllers-part 3: Programming languages . IEC 61131 - 61133 . International Electrotechnical Commission. 1993. Programmable controllers-part 3: Programming languages. IEC 61131-3.","journal-title":"IEC"},{"key":"e_1_3_2_1_14_1","volume-title":"Andr\u00e1s V\u00f6r\u00f6s, Tam\u00e1s Bartha, Enrique Blanco Vi\u00f1uela, and V\u00edctor M. Gonz\u00e1lez Su\u00e1rez.","author":"Darvas D\u00e1niel","year":"2014","unstructured":"D\u00e1niel Darvas , Borja Fern\u00e1ndez Adiego , Andr\u00e1s V\u00f6r\u00f6s, Tam\u00e1s Bartha, Enrique Blanco Vi\u00f1uela, and V\u00edctor M. Gonz\u00e1lez Su\u00e1rez. 2014 . Formal Verification of Complex Properties on PLC Programs. In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 284\u2013299. isbn:978-3-662-43613-4 D\u00e1niel Darvas, Borja Fern\u00e1ndez Adiego, Andr\u00e1s V\u00f6r\u00f6s, Tam\u00e1s Bartha, Enrique Blanco Vi\u00f1uela, and V\u00edctor M. Gonz\u00e1lez Su\u00e1rez. 2014. Formal Verification of Complex Properties on PLC Programs. In Formal Techniques for Distributed Objects, Components, and Systems, Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 284\u2013299. isbn:978-3-662-43613-4"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.18429\/JACoW-ICALEPCS2015-WEPGF092"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99840-4_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.1678428"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)40537-4"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2894026"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4493-7_25"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00665-z"},{"key":"e_1_3_2_1_27_1","unstructured":"Jaeseo Lee Sangki Kim and Kyungmin Bae. 2022. Supplementary material. https:\/\/github.com\/postechsv\/plc-release \t\t\t\t  Jaeseo Lee Sangki Kim and Kyungmin Bae. 2022. Supplementary material. https:\/\/github.com\/postechsv\/plc-release"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"e_1_3_2_1_29_1","unstructured":"Jingyue Li Altin Qeriqi Martin Steffen and Ingrid Chieh Yu. 2016. Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. In Norsk IKT-konferanse for forskning og utdanning. \t\t\t\t  Jingyue Li Altin Qeriqi Martin Steffen and Ingrid Chieh Yu. 2016. Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. In Norsk IKT-konferanse for forskning og utdanning."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)36116-5"},{"volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna Zohar","key":"e_1_3_2_1_31_1","unstructured":"Zohar Manna and Amir Pnueli . 1995. Temporal Verification of Reactive Systems: Safety . Springer-Verlag, Berlin , Heidelberg . isbn:0387944591 Zohar Manna and Amir Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, Berlin, Heidelberg. isbn:0387944591"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_11"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.10"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.1998.694666"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.001"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.05.002"},{"key":"e_1_3_2_1_41_1","unstructured":"Straton. 2022. Straton PLC. https:\/\/straton-plc.com\/en \t\t\t\t  Straton. 2022. Straton PLC. https:\/\/straton-plc.com\/en"},{"key":"e_1_3_2_1_42_1","unstructured":"Kun Wang Jingyi Wang Christopher M Poskitt Xiangxiang Chen Jun Sun and Peng Cheng. 2022. K-ST: A Formal Executable Semantics of PLC Structured Text Language. arXiv preprint arXiv:2202.04076. \t\t\t\t  Kun Wang Jingyi Wang Christopher M Poskitt Xiangxiang Chen Jun Sun and Peng Cheng. 2022. K-ST: A Formal Executable Semantics of PLC Structured Text Language. arXiv preprint arXiv:2202.04076."},{"key":"e_1_3_2_1_43_1","volume-title":"Proc. International Workshop on Rewriting Logic and its Applications.","author":"Yu Geunyeol","year":"2020","unstructured":"Geunyeol Yu and Kyungmin Bae . 2020 . Maude-SE: a Tight Integration of Maude and SMT Solvers . Proc. International Workshop on Rewriting Logic and its Applications. Geunyeol Yu and Kyungmin Bae. 2020. Maude-SE: a Tight Integration of Maude and SMT Solvers. Proc. International Workshop on Rewriting Logic and its Applications."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.36.8"}],"event":{"name":"FTSCS '22: 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Auckland New Zealand","acronym":"FTSCS '22"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568016","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563822.3568016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:07Z","timestamp":1750186807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,29]]},"references-count":44,"alternative-id":["10.1145\/3563822.3568016","10.1145\/3563822"],"URL":"https:\/\/doi.org\/10.1145\/3563822.3568016","relation":{},"subject":[],"published":{"date-parts":[[2022,11,29]]},"assertion":[{"value":"2022-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}