{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:21Z","timestamp":1780994361679,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T00:00:00Z","timestamp":1555372800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["FA8750-18-C-0092"],"award-info":[{"award-number":["FA8750-18-C-0092"]}]},{"DOI":"10.13039\/100011030","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-OE0000780"],"award-info":[{"award-number":["DE-OE0000780"]}],"id":[{"id":"10.13039\/100011030","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006642","name":"U.S. Department of Education","doi-asserted-by":"publisher","award":["GAANN Fellowship"],"award-info":[{"award-number":["GAANN Fellowship"]}],"id":[{"id":"10.13039\/100006642","id-type":"DOI","asserted-by":"publisher"}]},{"name":"AFOSR","award":["FA9550-16-1-0288"],"award-info":[{"award-number":["FA9550-16-1-0288"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,4,16]]},"DOI":"10.1145\/3302509.3311036","type":"proceedings-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T18:38:43Z","timestamp":1554403123000},"page":"47-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["HyPLC"],"prefix":"10.1145","author":[{"given":"Luis","family":"Garcia","sequence":"first","affiliation":[{"name":"University of California"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,4,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/28.216550"},{"key":"e_1_3_2_1_2_1","unstructured":"\"ABB launches new Pluto programmable logic controller for rail safety applications.\" {Online}. Available: http:\/\/www.abb.com\/cawp\/seitp202\/fa405fb9803dd9eac1258035002f53c0.aspx  \"ABB launches new Pluto programmable logic controller for rail safety applications.\" {Online}. Available: http:\/\/www.abb.com\/cawp\/seitp202\/fa405fb9803dd9eac1258035002f53c0.aspx"},{"key":"e_1_3_2_1_3_1","volume-title":"California. Naval Postgraduate School","author":"Kesler B.","year":"2011"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0954-1810(97)10002-4"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/37.272781"},{"key":"e_1_3_2_1_6_1","first-page":"907","volume-title":"JACoW","author":"Darvas D.","year":"2015"},{"key":"e_1_3_2_1_7_1","first-page":"106","volume-title":"Proceedings of the 11th Euromicro Conference on. IEEE","author":"Mader A.","year":"1999"},{"key":"e_1_3_2_1_8_1","first-page":"228","volume-title":"Control and Automation, 2005 and International Conference on Intelligent Agents, Web Technologies and Internet Commerce, International Conference on","volume":"2","author":"Thapa D.","year":"2005"},{"key":"e_1_3_2_1_9_1","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic,\" in Protocol Specification","author":"Gerth R.","year":"1995","journal-title":"Testing and Verification XV. Springer"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_11_1","first-page":"527","volume-title":"Springer","author":"Fulton N.","year":"2015"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9385-1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"A. Platzer Logical Foundations of Cyber-Physical Systems. Switzerland: Springer 2018.   A. Platzer Logical Foundations of Cyber-Physical Systems. Switzerland: Springer 2018.","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_2_1_15_1","volume-title":"Springer Science & Business Media","author":"John K.-H.","year":"2010"},{"key":"e_1_3_2_1_16_1","unstructured":"\"Antlr.\" {Online}. Available: https:\/\/www.antlr.org\/  \"Antlr.\" {Online}. Available: https:\/\/www.antlr.org\/"},{"key":"e_1_3_2_1_17_1","first-page":"31","volume-title":"2016 International Workshop on. IEEE","author":"Mathur A. P.","year":"2016"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.3311\/PPee.9743"},{"key":"e_1_3_2_1_19_1","first-page":"234","volume-title":"Proceedings of the 1998","volume":"1","author":"Rausch M.","year":"1998"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"S. E. McLaughlin S. A. Zonouz D. J. Pohly and P. D. McDaniel \"A trusted safety verifier for process controller code.\" in NDSS vol. 14 2014.  S. E. McLaughlin S. A. Zonouz D. J. Pohly and P. D. McDaniel \"A trusted safety verifier for process controller code.\" in NDSS vol. 14 2014.","DOI":"10.14722\/ndss.2014.23043"},{"key":"e_1_3_2_1_21_1","unstructured":"O. Pavlovic R. Pinger and M. Kollmann \"Automated formal verification of PLC programs written in IL \" in Conference on Automated Deduction (CADE) 2007 pp. 152--163.  O. Pavlovic R. Pinger and M. Kollmann \"Automated formal verification of PLC programs written in IL \" in Conference on Automated Deduction (CADE) 2007 pp. 152--163."},{"key":"e_1_3_2_1_22_1","first-page":"2700","volume-title":"2001 IEEE International Conference on","volume":"4","author":"Mertke T.","year":"2001"},{"key":"e_1_3_2_1_23_1","first-page":"911","volume-title":"JACoW","author":"Darvas D.","year":"2015"},{"key":"e_1_3_2_1_24_1","first-page":"311","volume-title":"Springer","author":"Tapken J.","year":"1998"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11563228_23"},{"key":"e_1_3_2_1_26_1","first-page":"1","volume-title":"2016 11th IEEE Symposium on. IEEE","author":"Darvas D.","year":"2016"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2006.11.001"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_3_2_1_29_1","first-page":"1564","article-title":"Compositional equivalence checking for models and code of control systems","volume":"12","author":"Majumdar R.","year":"2013","journal-title":"CDC. IEEE"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302509.3311036"},{"key":"e_1_3_2_1_31_1","unstructured":"Rockwell Automation \"Logix5000 controllers tasks programs and routines \" 2018. {Online}. Available: https:\/\/literature.rockwellautomation.com\/idc\/groups\/literature\/documents\/pm\/1756-pm005_-en-p.pdf  Rockwell Automation \"Logix5000 controllers tasks programs and routines \" 2018. {Online}. Available: https:\/\/literature.rockwellautomation.com\/idc\/groups\/literature\/documents\/pm\/1756-pm005_-en-p.pdf"},{"key":"e_1_3_2_1_32_1","unstructured":"M. d. Sousa \"MATIEC-IEC 61131-3 compiler \" 2014. {Online}. Available: https:\/\/bitbucket.org\/mjsousa\/matiec  M. d. Sousa \"MATIEC-IEC 61131-3 compiler \" 2014. {Online}. Available: https:\/\/bitbucket.org\/mjsousa\/matiec"},{"key":"e_1_3_2_1_33_1","first-page":"1","volume-title":"USA: Springer","author":"Goh J.","year":"2016"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0241-z"}],"event":{"name":"ICCPS '19: ACM\/IEEE 10th International Conference on Cyber-Physical Systems","location":"Montreal Quebec Canada","acronym":"ICCPS '19","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","IEEE-CS\\TCRT TC on Real-Time Systems"]},"container-title":["Proceedings of the 10th ACM\/IEEE International Conference on Cyber-Physical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3302509.3311036","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302509.3311036","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302509.3311036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:55Z","timestamp":1750204435000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3302509.3311036"}},"subtitle":["hybrid programmable logic controller program translation for verification"],"short-title":[],"issued":{"date-parts":[[2019,4,16]]},"references-count":34,"alternative-id":["10.1145\/3302509.3311036","10.1145\/3302509"],"URL":"https:\/\/doi.org\/10.1145\/3302509.3311036","relation":{},"subject":[],"published":{"date-parts":[[2019,4,16]]},"assertion":[{"value":"2019-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}