{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:26Z","timestamp":1776305246461,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,6,5]],"date-time":"2011-06-05T00:00:00Z","timestamp":1307232000000},"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":[[2011,6,5]]},"DOI":"10.1145\/2024724.2024843","type":"proceedings-article","created":{"date-parts":[[2011,9,6]],"date-time":"2011-09-06T15:10:46Z","timestamp":1315321846000},"page":"510-515","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Formal hardware\/software co-verification by interval property checking with abstraction"],"prefix":"10.1145","author":[{"given":"Minh D.","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of Kaiserslautern"}]},{"given":"Markus","family":"Wedler","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern"}]},{"given":"Dominik","family":"Stoffel","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern"}]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern"}]}],"member":"320","published-online":{"date-parts":[[2011,6,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Aquarius: a pipelined RISC CPU. Technical report","author":"Aitch T.","year":"2003","unstructured":"T. Aitch . Aquarius: a pipelined RISC CPU. Technical report , 2003 . T. Aitch. Aquarius: a pipelined RISC CPU. Technical report, 2003."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2007.76"},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes In Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Progress on the state explosion problem in model checking","author":"Clarke E.","year":"2001","unstructured":"E. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Progress on the state explosion problem in model checking . Lecture Notes In Computer Science , pages 176 -- 194 , 2001 . E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Progress on the state explosion problem in model checking. Lecture Notes In Computer Science, pages 176--194, 2001."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.82"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127908.1127920"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/996070.1009924"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.907270"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/513829.513839"},{"key":"e_1_3_2_1_12_1","volume-title":"Computer-Aided Verification of Coordinating Processes -- The Automata-Theoretic Approach","author":"Kurshan R. P.","year":"1994","unstructured":"R. P. Kurshan . Computer-Aided Verification of Coordinating Processes -- The Automata-Theoretic Approach . Princeton University Press, Princeton , New Jersey , 1994 . R. P. Kurshan. Computer-Aided Verification of Coordinating Processes -- The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994."},{"key":"e_1_3_2_1_13_1","first-page":"09","article-title":"Complete verification of weakly programmable ips against their operational isa model","author":"Loitz S.","year":"2010","unstructured":"S. Loitz , M. Wedler , D. Stoffel , C. Brehm , W. Kunz , and N. Wehn . Complete verification of weakly programmable ips against their operational isa model . In Proc. Forum on Specification & Design Languages , 09 2010 . S. Loitz, M. Wedler, D. Stoffel, C. Brehm, W. Kunz, and N. Wehn. Complete verification of weakly programmable ips against their operational isa model. In Proc. Forum on Specification & Design Languages, 09 2010.","journal-title":"Proc. Forum on Specification & Design Languages"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2006092"},{"key":"e_1_3_2_1_15_1","unstructured":"Onespin Solutions GmbH Germany. OneSpin 360MV. http:\/\/www.onespin-solutions.com.  Onespin Solutions GmbH Germany. OneSpin 360MV. http:\/\/www.onespin-solutions.com."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040317"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. Forum on Design Languages","author":"Schickel M.","year":"2006","unstructured":"M. Schickel , V. Nimbler , M. Braun , and H. Eveking . On consistency and completeness of property sets: Exploiting the property-based design process . In Proc. Forum on Design Languages , 2006 . M. Schickel, V. Nimbler, M. Braun, and H. Eveking. On consistency and completeness of property sets: Exploiting the property-based design process. In Proc. Forum on Design Languages, 2006."},{"key":"e_1_3_2_1_18_1","first-page":"207","volume-title":"Formal Methods in Computer Aided Design","author":"Urdahl J.","year":"2010","unstructured":"J. Urdahl , D. Stoffel , J. Bormann , M. Wedler , and W. Kunz . Path predicate abstraction by complete interval property checking . In Formal Methods in Computer Aided Design , pages 207 -- 215 , 2010 . J. Urdahl, D. Stoffel, J. Bormann, M. Wedler, and W. Kunz. Path predicate abstraction by complete interval property checking. In Formal Methods in Computer Aided Design, pages 207--215, 2010."}],"event":{"name":"DAC '11: The 48th Annual Design Automation Conference 2011","location":"San Diego California","acronym":"DAC '11","sponsor":["EDAC Electronic Design Automation Consortium","SIGDA ACM Special Interest Group on Design Automation","IEEE Council on Electronic Design Automation (CEDA)"]},"container-title":["Proceedings of the 48th Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2024724.2024843","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2024724.2024843","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:07Z","timestamp":1750244767000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2024724.2024843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,5]]},"references-count":18,"alternative-id":["10.1145\/2024724.2024843","10.1145\/2024724"],"URL":"https:\/\/doi.org\/10.1145\/2024724.2024843","relation":{},"subject":[],"published":{"date-parts":[[2011,6,5]]},"assertion":[{"value":"2011-06-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}