{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:08:30Z","timestamp":1767262110750,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106245","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"326-336","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Symbolic execution of programmable logic controller code"],"prefix":"10.1145","author":[{"given":"Shengjian","family":"Guo","sequence":"first","affiliation":[{"name":"Virginia Tech, USA"}]},{"given":"Meng","family":"Wu","sequence":"additional","affiliation":[{"name":"Virginia Tech, USA"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691588"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_10"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.57"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25423-4_15"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660200"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1929004.1929006"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351741"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41010-9_9"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1434790.1434807"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2016.7497884"},{"key":"e_1_3_2_1_12_1","first-page":"224","volume-title":"USENIX Symposium on Operating Systems Design and Implementation","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R. Engler . KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs . In USENIX Symposium on Operating Systems Design and Implementation , pages 209\u2013 224 , 2008 . Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation, pages 209\u2013224, 2008."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2011.2182653"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682939"},{"key":"e_1_3_2_1_15_1","first-page":"80","volume-title":"International Conference on Formal Methods in Computer-Aided Design","author":"Chaki Sagar","year":"2011","unstructured":"Sagar Chaki , Arie Gurfinkel , and Ofer Strichman . Time-bounded analysis of real-time systems . In International Conference on Formal Methods in Computer-Aided Design , pages 72\u2013 80 , 2011 . Sagar Chaki, Arie Gurfinkel, and Ofer Strichman. Time-bounded analysis of real-time systems. In International Conference on Formal Methods in Computer-Aided Design, pages 72\u201380, 2011."},{"issue":"1","key":"e_1_3_2_1_16_1","first-page":"30","article-title":"PLC program verification and analysis using the coq theorem prover","volume":"46","author":"Gang","year":"2010","unstructured":"Gang chen, Xiaoyu Song , and Ming Gu . PLC program verification and analysis using the coq theorem prover . Acta Scientiarum Naturalium Universitatis Pekinensis , 46 ( 1 ): 30 \u2013 34 , 2010 . Gang chen, Xiaoyu Song, and Ming Gu. PLC program verification and analysis using the coq theorem prover. Acta Scientiarum Naturalium Universitatis Pekinensis, 46(1):30\u201334, 2010.","journal-title":"Acta Scientiarum Naturalium Universitatis Pekinensis"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_6"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_36"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713257"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"e_1_3_2_1_21_1","first-page":"181","volume-title":"International Symposium on Formal Methods for Components and Objects","author":"Deng Xianghua","year":"2002","unstructured":"Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Georg Jung , Robby, and Gurdip Singh . Model-checking middleware-based event-driven real-time embedded software . In International Symposium on Formal Methods for Components and Objects , pages 154\u2013 181 , 2002 . Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, and Gurdip Singh. Model-checking middleware-based event-driven real-time embedded software. In International Symposium on Formal Methods for Components and Objects, pages 154\u2013181, 2002."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2011.6058983"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmsy.2014.04.008"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970332"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786841"},{"key":"e_1_3_2_1_27_1","first-page":"4","volume-title":"International Symposium on Advanced Topics in Electrical Engineering","author":"Haba C. G.","year":"2011","unstructured":"C. G. Haba , R. Cociu , and L. Cociu . Mixed mode verification of PLC based control systems . In International Symposium on Advanced Topics in Electrical Engineering , pages 1\u2013 4 , 2011 . C. G. Haba, R. Cociu, and L. Cociu. Mixed mode verification of PLC based control systems. In International Symposium on Advanced Topics in Electrical Engineering, pages 1\u20134, 2011."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11925040_11"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-12015-2","volume-title":"IEC 61131-3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids","author":"John Karl-Heinz","year":"2010","unstructured":"Karl-Heinz John and Michael Tiegelkamp . IEC 61131-3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids . Springer Science & amp; Business Media, 2010 . Karl-Heinz John and Michael Tiegelkamp. IEC 61131-3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids. Springer Science & Business Media, 2010."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207543.2010.492404"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2755753.2755803"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642998"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.3103\/S0146411615070159"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_4"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_33"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1186\/s13639-015-0020-8"},{"key":"e_1_3_2_1_39_1","unstructured":"IEC 61131-3 compiler. IEC 61131-3 compiler."},{"key":"e_1_3_2_1_40_1","volume-title":"Network and Distributed System Security Symposium","author":"McLaughlin Stephen E.","year":"2014","unstructured":"Stephen E. McLaughlin , Saman A. Zonouz , Devin J. Pohly , and Patrick D . McDaniel. A trusted safety verifier for process controller code . In Network and Distributed System Security Symposium , 2014 . Stephen E. McLaughlin, Saman A. Zonouz, Devin J. Pohly, and Patrick D. McDaniel. A trusted safety verifier for process controller code. In Network and Distributed System Security Symposium, 2014."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.2050199"},{"key":"e_1_3_2_1_42_1","first-page":"78","volume-title":"Formalisms for Reuse and Systems Integration","author":"Nellen Johanna","unstructured":"Johanna Nellen , Erika \u00c1brah\u00e1m , and Benedikt Wolters . A CEGAR tool for the reachability analysis of PLC-controlled plants using hybrid automata . In Formalisms for Reuse and Systems Integration , pages 55\u2013 78 . 2015. Johanna Nellen, Erika \u00c1brah\u00e1m, and Benedikt Wolters. A CEGAR tool for the reachability analysis of PLC-controlled plants using hybrid automata. In Formalisms for Reuse and Systems Integration, pages 55\u201378. 2015."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10796-016-9671-9"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1516744.1516792"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792772"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCI-CC.2013.6622270"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSESS.2014.6933545"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Paderborn Germany","acronym":"ESEC\/FSE'17"},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106245","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:36Z","timestamp":1750217436000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106245"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":49,"alternative-id":["10.1145\/3106237.3106245","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106245","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}