{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:13Z","timestamp":1740122713329,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,9,19]],"date-time":"2017-09-19T00:00:00Z","timestamp":1505779200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s10703-017-0299-2","type":"journal-article","created":{"date-parts":[[2017,9,19]],"date-time":"2017-09-19T10:41:45Z","timestamp":1505817705000},"page":"395-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A methodology to take credit for high-level verification during RTL verification"],"prefix":"10.1007","volume":"51","author":[{"given":"Frederic","family":"Doucet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4232-6530","authenticated-orcid":false,"given":"Robert","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,19]]},"reference":[{"key":"299_CR1","volume-title":"Computer-aided verification of coordinating processes","author":"RP Kurshan","year":"1994","unstructured":"Kurshan RP (1994) Computer-aided verification of coordinating processes. Princeton University Press, Princeton"},{"key":"299_CR2","doi-asserted-by":"crossref","unstructured":"Kurshan RP (2008) Verification technology transfer. In: 25 Years of model checking, LNCS no. 5000, Springer, pp 46\u201364","DOI":"10.1007\/978-3-540-69850-0_3"},{"issue":"2","key":"299_CR3","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/2951860.2951873","volume":"47","author":"R Bloem","year":"2016","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2016) Decidability of parameterized verification. ACM SIGACT News 47(2):53\u201364","journal-title":"ACM SIGACT News"},{"key":"299_CR4","unstructured":"Konnov I, Kotek T, Wang Q, Veith H, Bliudze S, Sifakis J (2016) Parameterized systems in BIP: design and model checking. In: Desharnais J, Jagadeesan R (eds) 27th International conference on concurrency theory (CONCUR 2016), volume 59 of Leibniz international proceedings in informatics (LIPIcs). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, pp 30:1\u201330:16"},{"key":"299_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2200\/S00658ED1V01Y201508DCT013","volume":"6","author":"R Bloem","year":"2015","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2015) Decidability of parameterized verification. Synth Lect Distributed Comput Theory 6:1\u2013170","journal-title":"Synth Lect Distributed Comput Theory"},{"key":"299_CR6","doi-asserted-by":"crossref","unstructured":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H (2014) Parameterized model checking of rendezvous systems. In: Baldan P, Gorla D (eds) CONCUR 2014: concurrency theory, volume 8704 of lecture notes in computer science. Springer, Berlin, Heidelberg, pp 109\u2013124","DOI":"10.1007\/978-3-662-44584-6_9"},{"key":"299_CR7","doi-asserted-by":"crossref","unstructured":"John A, Konnov I, Schmid U, Veith H, Widder J (2013) Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201\u2013209","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"299_CR8","doi-asserted-by":"crossref","unstructured":"Berry G, Kishinevsky M, Singh S (2003) System-level design and verification using a synchronous language. In: ICCAD \u201903: proceedings of the 2003 IEEE\/ACM international conference on Computer-aided design. IEEE Computer Society, Washington, DC, USA, p 433","DOI":"10.1109\/ICCAD.2003.159720"},{"issue":"2","key":"299_CR9","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry G, Gonthier G (1992) The Esterel synchronous programming language: design, semantics, implementation. Sci Comput Program 19(2):87\u2013152","journal-title":"Sci Comput Program"},{"key":"299_CR10","volume-title":"The foundations of Esterel","author":"G Berry","year":"2000","unstructured":"Berry G (2000) The foundations of Esterel. MIT Press, Cambridge"},{"issue":"3","key":"299_CR11","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231\u2013274","journal-title":"Sci Comput Program"},{"issue":"4","key":"299_CR12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel D, Naamad A (1996) The STATEMATE semantics of statecharts. ACM Trans Softw Eng Methodol 5(4):293\u2013333","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"1","key":"299_CR13","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA (1999) Reactive modules. Form Methods Syst Des 15(1):7\u201348","journal-title":"Form Methods Syst Des"},{"key":"299_CR14","doi-asserted-by":"crossref","unstructured":"Alur R, Grosu R (2000) Modular refinement of hierarchical reactive machines. In: POPL \u201900: proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM Press, New York, NY, USA, pp 390\u2013402","DOI":"10.1145\/325694.325746"},{"issue":"2","key":"299_CR15","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/973097.973101","volume":"26","author":"R Alur","year":"2004","unstructured":"Alur R, Grosu R (2004) Modular refinement of hierarchic reactive machines. ACM Trans Program Lang Syst 26(2):339\u2013369","journal-title":"ACM Trans Program Lang Syst"},{"key":"299_CR16","unstructured":"Abdi S, Gajski D (2004) System-level verification with model algebra. CECS, UCI, Technical Report 04-29"},{"key":"299_CR17","unstructured":"Abdi S (2005) Functional verification of system-level model refinements. Ph.D. dissertation, University of California, Irvine"},{"issue":"1","key":"299_CR18","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/s10766-005-0001-y","volume":"34","author":"S Abdi","year":"2006","unstructured":"Abdi S, Gajski D (2006) Verification of system-level model transformations. Int J Parallel Program 34(1):29\u201359","journal-title":"Int J Parallel Program"},{"key":"299_CR19","doi-asserted-by":"crossref","unstructured":"Berry G, Ramesh S, Shyamasundar RK (1993) Communicating Reactive Processes. In: POPL","DOI":"10.1145\/158511.158526"},{"key":"299_CR20","doi-asserted-by":"crossref","unstructured":"Kollmann R, Gogolla M (2001) Capturing dynamic program behaviour with UML collaboration diagrams. In: Proceedings fifth European conference on software maintenance and reengineering, Lisbon, pp 58\u201367","DOI":"10.1109\/CSMR.2001.914969"},{"key":"299_CR21","doi-asserted-by":"crossref","unstructured":"Cartaxo EG, Neto FGO, Machado PDL (2007) Test case generation by means of UML sequence diagrams and labeled transition systems. In: 2007 in Proceedings of IEEE international conference on systems, man and cybernetics, Montreal, pp 1292\u20131297","DOI":"10.1109\/ICSMC.2007.4414060"},{"key":"299_CR22","unstructured":"Broy M, Kr\u00fcger I, Meisinger M (2004) Automotive software-connected services in mobile networks: first automotive software workshop, ASWSD 2004, San Diego, CA, USA, January 10\u201312, 2004, Revised selected papers, Broy M, Kr\u00fcger I, Meisinger M (eds), Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2006"},{"key":"299_CR23","doi-asserted-by":"crossref","unstructured":"Seiter J, Wille R, Kahne U, Drechsler R (2014) Automatic refinement checking for formal system models. In: Proceedings of the 2014 forum on specification and design languages (FDL), Munich, pp 1\u20138","DOI":"10.1109\/FDL.2014.7119339"},{"key":"299_CR24","volume-title":"System design with SystemC","author":"T Groetker","year":"2002","unstructured":"Groetker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer Academic Publishers, Dordrecht"},{"key":"299_CR25","doi-asserted-by":"crossref","unstructured":"Flaisher A, Gluska A, Singerman E (2007) Case study: integrating fv and dv in the verification of the intel core 2 duo microprocessor. In: FMCAD \u201907: proceedings of the formal methods in computer aided design. IEEE Computer Society, Washington, DC, USA, pp 192\u2013195","DOI":"10.1109\/FAMCAD.2007.38"},{"key":"299_CR26","doi-asserted-by":"crossref","unstructured":"Beers R (2008) Pre-RTL formal verification: an intel experience. In: DAC \u201908: proceedings of the 45th annual design automation conference. ACM, New York, NY, USA, pp 806\u2013811","DOI":"10.1145\/1391469.1391675"},{"key":"299_CR27","doi-asserted-by":"crossref","unstructured":"Gluska A, Libis L (2009) Shortening the verification cycle with synthesizable abstract models. In: DAC \u201909: proceedings of the 46th annual design automation conference. ACM, New York, NY, USA, pp 454\u2013459","DOI":"10.1145\/1629911.1630032"},{"key":"299_CR28","unstructured":"Grobe D, Peraza H, Klingauf W, Drechsler R (2008) Measuring the quality of a SystemC Testbench by using code coverage techniques. In: Embedded systems specification and design languages: selected contributions from FDL\u201907. Springer, Netherlands, pp 73\u201386"},{"issue":"1s","key":"299_CR29","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/2435227.2435257","volume":"12","author":"P Herber","year":"2013","unstructured":"Herber P, Glesner S (2013) A HW\/SW co-verification framework for SystemC. ACM Trans Embed Comput Syst 12(1s):61","journal-title":"ACM Trans Embed Comput Syst"},{"key":"299_CR30","doi-asserted-by":"crossref","unstructured":"Junior AD, da Silva DJC (2007) Code-coverage based test vector generation for SystemC designs. In: IEEE computer society annual symposium on VLSI (ISVLSI \u201907), Porto Alegre, pp 198\u2013206","DOI":"10.1109\/ISVLSI.2007.31"},{"key":"299_CR31","doi-asserted-by":"crossref","unstructured":"Lin B, Yang Z, Cong K, Xie F (2016) Generating high coverage tests for SystemC designs using symbolic execution. In: Design automation conference (ASP-DAC) 2016 21st Asia and South Pacific, pp 166\u2013171","DOI":"10.1109\/ASPDAC.2016.7428006"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0299-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0299-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0299-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T13:53:40Z","timestamp":1570110820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0299-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,19]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["299"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0299-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,9,19]]}}}