{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T13:47:39Z","timestamp":1719755259983},"reference-count":19,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2017]]},"DOI":"10.1587\/transinf.2016edp7452","type":"journal-article","created":{"date-parts":[[2017,7,31]],"date-time":"2017-07-31T18:19:36Z","timestamp":1501525176000},"page":"1819-1826","source":"Crossref","is-referenced-by-count":10,"title":["Model Checking of Embedded Assembly Program Based on Simulation"],"prefix":"10.1587","volume":"E100.D","author":[{"given":"Satoshi","family":"YAMANE","sequence":"first","affiliation":[{"name":"Graduate School of Natural Science and Technology, Kanazawa University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryosuke","family":"KONOSHITA","sequence":"additional","affiliation":[{"name":"Graduate School of Natural Science and Technology, Kanazawa University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomonori","family":"KATO","sequence":"additional","affiliation":[{"name":"Graduate School of Natural Science and Technology, Kanazawa University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999."},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] R. Jhana and R. Majumdar, \u201cSoftware model checking,\u201d ACM Comput. Surv., vol.41, no.4, 2009. 10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] L. de Moura and N. Bj<i>\u03d5<\/i>rner, \u201cZ3: An Efficient SMT Solver,\u201d LNCS 4963, pp.337-340, 2008. 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] E.M. Clarke, E.A. Emerson, and J. Sifakis, \u201cModel Checking: Algorithmic Verification and Debugging,\u201d Commun, ACM, vol.52, no.11, pp.74-84, 2009. 10.1145\/1592761.1592781","DOI":"10.1145\/1592761.1592781"},{"key":"5","unstructured":"[5] Corporation, R.E., Renesas Electronics, Renesas Electronics Corporation (online), http:\/\/japan.renesas.com\/, 2014."},{"key":"6","unstructured":"[6] nuvo WHEEL:ZMP, http:\/\/www.zmp.co.jp\/products\/wheel, 2016."},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] D. Beyer, T.A. Henzinger, R. Jhala, and R. Majumdar, \u201cThe software model checker Blast,\u201d International Journal on Software Tools for Technology Transfer, vol.9, no.5-6, pp.505-525, 2007. 10.1007\/s10009-007-0044-z","DOI":"10.1007\/s10009-007-0044-z"},{"key":"8","unstructured":"[8] G. Weissenbacher, The BOOP Toolkit v0.42, Graz University of Technology (online), available from http:\/\/boop.sourceforge.net\/ (accessed 2014-6-17)."},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] B. Schlich and S. Kowalewski, \u201cModel Checking C Source Code for Embedded Systems,\u201d International Journal on Software Tools for Technology Transfer, vol.11, no.3, pp.187-202, 2009. 10.1007\/s10009-009-0106-5","DOI":"10.1007\/s10009-009-0106-5"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] B. Schlich, \u201cModel Checking of Software for Microcontrollers,\u201d ACM Trans. Embed. Comput. Syst., vol.9, no.4, pp.1-27, 2010. 10.1145\/1721695.1721702","DOI":"10.1145\/1721695.1721702"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] B. Schlich, J. Brauer, and S. Kowalewski, \u201cApplication of Static Analyses for State-space Reduction to the Microcontroller Binary Code,\u201d Sci. Comput. Program., vol.76, no.2, pp.100-118, 2011. 10.1016\/j.scico.2010.03.006","DOI":"10.1016\/j.scico.2010.03.006"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] T. Noll and B. Schlich, \u201cDelayed Nondeterminism in Model Checking Embedded Systems Assembly Code,\u201d LNCS 4899, pp.185-201, 2008. 10.1007\/978-3-540-77966-7_16","DOI":"10.1007\/978-3-540-77966-7_16"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] G.J. Holzmann, \u201cThe Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited,\u201d LNCS 1680, pp.232-244, 1999. 10.1007\/3-540-48234-2_18","DOI":"10.1007\/3-540-48234-2_18"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] K. Yorav and O. Grumberg, \u201cStatic Analysis for StateSpace Reductions Preserving Temporal Logics,\u201d Form. Methods Syst. Des., vol.25, no.1, pp.67-96, 2004. 10.1023\/b:form.0000033963.55470.9e","DOI":"10.1023\/B:FORM.0000033963.55470.9e"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] L.I. Millett and T.Teitelbaum, \u201cIssues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation,\u201d International Journal on Software Tools for Technology Transfer, vol.2, no.4, pp.343-349, 2000. 10.1007\/s100090050041","DOI":"10.1007\/s100090050041"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] M.C. Browne, E.M. Clarke, and O. Gr\u00fcmberg, \u201cCharacterizing Kripke Structures in Temporal Logic,\u201d LNCS 249, pp.256-270, 1987. 10.1007\/3-540-17660-8_60","DOI":"10.1007\/3-540-17660-8_60"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] E.M. Clarke, E.A. Emerson, and A.P. Sistla, \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,\u201d ACM Trans. Program. Lang. Syst., vol.8, no.2, pp.244-263, 1986. 10.1145\/5397.5399","DOI":"10.1145\/5397.5399"},{"key":"18","unstructured":"[18] G. Klein, JFlex-The Fast Scanner Generator for Java, CSE UNSW (online), available from (http:\/\/jflex.de\/<i><\/i>) (accessed 2014-6-27)."},{"key":"19","unstructured":"[19] M.P. Jones, Jacc: just another compiler compiler for Java, Department of Computer Science and Engineering at the OGI School of Science &amp; Engineering at OHSU (online), available from (http:\/\/jflex.de\/<i><\/i>) (accessed 2014-6-27)."}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/8\/E100.D_2016EDP7452\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T17:36:27Z","timestamp":1569951387000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/8\/E100.D_2016EDP7452\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":19,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2017]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2016edp7452","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}