{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:18:10Z","timestamp":1750220290319,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T00:00:00Z","timestamp":1650844800000},"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":[[2022,4,25]]},"DOI":"10.1145\/3477314.3507121","type":"proceedings-article","created":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T00:37:36Z","timestamp":1651883856000},"page":"1827-1836","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques"],"prefix":"10.1145","author":[{"given":"Thuy","family":"Nguyen","sequence":"first","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Ishikawa, Japan"}]},{"given":"Takashi","family":"Tomita","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Ishikawa, Japan"}]},{"given":"Junpei","family":"Endo","sequence":"additional","affiliation":[{"name":"AISIN SOFTWARE Co., Ltd, Nagoya, Japan"}]},{"given":"Geon-ung","family":"Kang","sequence":"additional","affiliation":[{"name":"AISIN SOFTWARE Co., Ltd, Nagoya, Japan"}]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Ishikawa, Japan"}]}],"member":"320","published-online":{"date-parts":[[2022,5,6]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2008. The CBMC Homepage. https:\/\/www.cprover.org\/cbmc\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2010. The CPROVER Manual. http:\/\/www.cprover.org\/cprover-manual\/cbmc\/unwinding\/"},{"key":"e_1_3_2_1_3_1","unstructured":"2013. Boom. https:\/\/www.cprover.org\/boom\/"},{"key":"e_1_3_2_1_4_1","unstructured":"2015. Eva an Evolved Value Analysis. https:\/\/frama-c.com\/fc-plugins\/eva.html"},{"key":"e_1_3_2_1_5_1","unstructured":"2017. Cobra Static Code Analyzer. https:\/\/spinroot.com\/cobra\/"},{"key":"e_1_3_2_1_6_1","unstructured":"2019. SEI CERT C Coding Standard - SEI CERT C Coding Standard - Confluence. https:\/\/wiki.sei.cmu.edu\/confluence\/display\/c\/SEI+CERT+C+Coding+Standard"},{"key":"e_1_3_2_1_7_1","unstructured":"2021. Hardware manual of STM32F101xx. https:\/\/www.st.com\/content\/ccc\/resource\/technical\/document\/reference_manual\/59\/b9\/ba\/7f\/11\/af\/43\/d5\/CD00171190.pdf\/files\/CD00171190.pdf\/jcr:content\/translations\/en.CD00171190.pdf"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Basler Alastair Donaldson Alexander Kaiser Daniel Kroening Michael Tautschnig and Thomas Wahl. 2012. SatAbs: A bit-precise verifier for C programs (competition contribution). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7214 LNCS (2012) 552--555.","DOI":"10.1007\/978-3-642-28756-5_47"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"A Biere A Cimatti EM Clarke O Strichman and Y Zhu. 2003. Bounded model checking. (2003). https:\/\/kilthub.cmu.edu\/articles\/Bounded_Model_Checking\/6603944\/files\/12094325.pdf","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Sandrine Blazy David B\u00fchler and Boris Yakobowski. 2017. Structuring Abstract Interpreters Through State and Value Abstractions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10145 LNCS (2017) 112--130. https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-52234-0_7","DOI":"10.1007\/978-3-319-52234-0_7"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597809.2597823"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"volume-title":"Logics and Languages for Reliability and Security","author":"Cousot Patrick","key":"e_1_3_2_1_16_1","unstructured":"Patrick Cousot and Radhia Cousot. 2010. A gentle introduction to formal verification of computer systems by abstract interpretation. In Logics and Languages for Reliability and Security. IOS Press, 1--29."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Ansgar Fehnker Ralf Huuck Bastian Schlich and Michael Tapp. 2009. Automatic bug detection in microcontroller software by static program analysis. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5404 LNCS (2009) 267--278.","DOI":"10.1007\/978-3-540-95891-8_26"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092313"},{"key":"e_1_3_2_1_20_1","volume-title":"The power of ten-rules for developing safety critical code1. Software Technology 10","author":"Holzmann Gerard J","year":"2018","unstructured":"Gerard J Holzmann. 2018. The power of ten-rules for developing safety critical code1. Software Technology 10 (2018)."},{"key":"e_1_3_2_1_21_1","volume-title":"Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers. Software Testing, Verification and Reliability (8","author":"Nguyen Thuy","year":"2021","unstructured":"Thuy Nguyen, Takashi Tomita, Junpei Endo, and Toshiaki Aoki. 2021. Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers. Software Testing, Verification and Reliability (8 2021), e1788."},{"key":"e_1_3_2_1_22_1","unstructured":"Dan Saks. 2002. Representing and Manipulating Hardware in Standard C and C++. (2002)."},{"key":"e_1_3_2_1_23_1","article-title":"Model checking of software for microcontrollers","volume":"9","author":"Schlich Bastian","year":"2010","unstructured":"Bastian Schlich. 2010. Model checking of software for microcontrollers. Transactions on Embedded Computing Systems 9, 4 (3 2010).","journal-title":"Transactions on Embedded Computing Systems"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Ole Tange. 2020. GNU Parallel 20200622 ('Floyd'). GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them. 10.5281\/zenodo.3903853","DOI":"10.5281\/zenodo.3903853"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363387"}],"event":{"name":"SAC '22: The 37th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Virtual Event","acronym":"SAC '22"},"container-title":["Proceedings of the 37th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3507121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477314.3507121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:29Z","timestamp":1750188689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3507121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,25]]},"references-count":25,"alternative-id":["10.1145\/3477314.3507121","10.1145\/3477314"],"URL":"https:\/\/doi.org\/10.1145\/3477314.3507121","relation":{},"subject":[],"published":{"date-parts":[[2022,4,25]]},"assertion":[{"value":"2022-05-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}