{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T21:07:35Z","timestamp":1672348055533},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2007,9,21]],"date-time":"2007-09-21T00:00:00Z","timestamp":1190332800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2007,11,1]]},"DOI":"10.1007\/s10836-007-5015-5","type":"journal-article","created":{"date-parts":[[2007,9,20]],"date-time":"2007-09-20T10:46:28Z","timestamp":1190285188000},"page":"373-388","source":"Crossref","is-referenced-by-count":3,"title":["Too Few or Too Many Properties? Measure it by ATPG!"],"prefix":"10.1007","volume":"23","author":[{"given":"Franco","family":"Fummi","sequence":"first","affiliation":[]},{"given":"Graziano","family":"Pravadelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,9,21]]},"reference":[{"key":"5015_CR1","doi-asserted-by":"crossref","unstructured":"Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) FoCs\u2014Automatic generation of simulation checkers from formal specifications. In: Proc. of CAV, vol\u00a01855 of LNCS. Springer-Verlag, pp\u00a0538\u2013542","DOI":"10.1007\/10722167_40"},{"key":"5015_CR2","doi-asserted-by":"crossref","unstructured":"Cheng K-T, Jou J-Y (1990) A single-state-transition fault model for sequential machines. In: Proc. of IEEE ICCAD, pp\u00a0226\u2013229","DOI":"10.1109\/ICCAD.1990.129887"},{"key":"5015_CR3","unstructured":"Clarke E, Grumberg D, Peled D (2000) Model checking. MIT Press"},{"key":"5015_CR4","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, McMillan K, Zhao X (1995) Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. of ACM\/IEEE DAC, pp\u00a0427\u2013432","DOI":"10.1145\/217474.217565"},{"key":"5015_CR5","doi-asserted-by":"crossref","unstructured":"Chockler H, Kupferman O, Kurshan RP, Vardi MY (2001) A practical approach to coverage in model checking. In: Proc. of CAV, pp\u00a066\u201378","DOI":"10.1007\/3-540-44585-4_7"},{"key":"5015_CR6","first-page":"528","volume-title":"Proc. of international conference on tools and algorithms for the construction and analysis of systems, vol\u00a02031 of LNCS","author":"H Chockler","year":"2001","unstructured":"Chockler H, Kupferman O, Vardi MY (2001) Coverage metrics for temporal logic model checking. In: Proc. of international conference on tools and algorithms for the construction and analysis of systems, vol\u00a02031 of LNCS. Springer, New York, NY, pp\u00a0528\u2013542"},{"key":"5015_CR7","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-540-39724-3_11","volume-title":"Correct hardware design and verification methods, vol\u00a02860 of LNCS","author":"H Chockler","year":"2003","unstructured":"Chockler H, Kupferman O, Vardi MY (2003) Coverage metrics for formal verification. In: Correct hardware design and verification methods, vol\u00a02860 of LNCS. Springer, New York, NY, pp\u00a0111\u2013125"},{"key":"5015_CR8","unstructured":"Department of Electrical and Computer Engineering at the University of Texas, Austin (1999) Texas97 benchmarks. In: http:\/\/embedded.eecs.berkeley.edu\/research\/vis\/texas-97"},{"key":"5015_CR9","doi-asserted-by":"crossref","unstructured":"Di Guglielmo G, Fummi F, Marconcini C, Pravadelli G (2006) FATE: a functional ATPG to traverse unstabilized EFSMs. In: Proc. of IEEE ETS, pp\u00a0179\u2013184","DOI":"10.1109\/ETS.2006.21"},{"key":"5015_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E Emerson","year":"1985","unstructured":"Emerson E, Halpen J (1985) Decision procedures and expressiveness in the temporal logic of branching time. J Comput Syst Sci 30:1\u201324","journal-title":"J Comput Syst Sci"},{"key":"5015_CR11","unstructured":"Fedeli A, Fummi F, Pravadelli G, Rossi U, Toto F (2003) On the use of a high-level fault model to check properties incompleteness. In: Proc. of ACM\/IEEE MEMOCODE, pp\u00a0145\u2013152"},{"key":"5015_CR12","unstructured":"Ferrandi F, Fummi F, Gerli L, Sciuto D (1999) Symbolic functional vector generation for VHDL specifications. In: Proc. of IEEE DATE, pp\u00a0442\u2013446"},{"key":"5015_CR13","unstructured":"Fin A, Fummi F (2003) Laerte++: an object oriented high-level TPG for systemC designs. In: Languages for system specification: Selected contributions on UML, systemC, system Verilog, mixed-signal systems, and property specification from FDL\u201903, pp\u00a0105\u2013107"},{"issue":"4","key":"5015_CR14","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/MDT.2003.1214351","volume":"20","author":"I Harris","year":"2003","unstructured":"Harris I (2003) Fault models and test generation for hardware-software covalidation. IEEE Des Test Comput 20(4):40\u201347","journal-title":"IEEE Des Test Comput"},{"key":"5015_CR15","unstructured":"Hoskote Y, Kam T, Ho PH, Zao X (1999) Coverage estimation for symbolic model checking. In: Proc. of ACM\/IEEE DAC, pp\u00a0300\u2013305"},{"key":"5015_CR16","doi-asserted-by":"crossref","unstructured":"Jayakumar N, Purandare M, Somenzi F (2003) Dos and don\u2019ts of CTL state coverage estimation. In: Proc. of ACM\/IEEE DAC, pp\u00a0292\u2013295","DOI":"10.1145\/775832.775908"},{"key":"5015_CR17","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct hardware design and verification methods, vol\u00a01703 of LNCS","author":"S Katz","year":"1999","unstructured":"Katz S, Grumberg O, Geist D (1999) Have I written enough properties? - A method of comparison between specification and implementation. In: Correct hardware design and verification methods, vol\u00a01703 of LNCS. Springer, New York, NY, pp\u00a0280\u2013297"},{"key":"5015_CR18","doi-asserted-by":"crossref","unstructured":"Lee T-C, Hsiung P-A (2004) Mutation coverage estimation for model checking. In: Proc. of international symposium on automated technology for verification and analysis, vol\u00a03299 of LNCS. Springer, pp\u00a0534\u2013368","DOI":"10.1007\/978-3-540-30476-0_29"},{"key":"5015_CR19","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein O, Pnueli A (2000) Propositional temporal logics: decidability and completeness. Log J IGPL 8:55\u201385","journal-title":"Log J IGPL"},{"key":"5015_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Norwell, MA"},{"key":"5015_CR21","unstructured":"Politecnico\u00a0di\u00a0Torino (1999) ITC-99 benchmarks. In: http:\/\/www.cad.polito.it\/tools\/itc99.html"},{"issue":"3","key":"5015_CR22","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.2307\/2695091","volume":"66","author":"M Reynolds","year":"2001","unstructured":"Reynolds M (2001) An axiomatization of full computation tree logic. J Symb Log 66(3):1011\u20131057","journal-title":"J Symb Log"},{"key":"5015_CR23","doi-asserted-by":"crossref","unstructured":"Santos MB, Gon\u00e7alves FM, Teixeira IC, Teixeira JP (2000) RTL-based functional test generation for high defects coverage in digital SoCs. In: Proc. of IEEE ETW, pp\u00a099\u2013104","DOI":"10.1109\/ETW.2000.873785"},{"issue":"4","key":"5015_CR24","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/54.936247","volume":"18","author":"S Taziran","year":"2001","unstructured":"Taziran S, Keutzer K (2001) Coverage metrics for functional validation of hardware design. IEEE Des Test Comput 18(4):36\u201345","journal-title":"IEEE Des Test Comput"},{"key":"5015_CR25","unstructured":"Xu X, Kimura S, Horikawa K, Tsuchiya T (2005) Transition traversal coverage estimation for symbolic model checking. In: Proc. of ACM\/IEEE MEMOCODE, pp\u00a0259\u201326"},{"key":"5015_CR26","doi-asserted-by":"crossref","unstructured":"Xu X, Kimura S, Horikawa K, Tsuchiya T (2006) Transition-based coverage estimation for symbolic model checking. In: Proc. of ACM\/IEEE ASP-DAC, pp\u00a01\u20136","DOI":"10.1145\/1118299.1118303"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-007-5015-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-007-5015-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-007-5015-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:57:42Z","timestamp":1559253462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-007-5015-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9,21]]},"references-count":26,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,11,1]]}},"alternative-id":["5015"],"URL":"https:\/\/doi.org\/10.1007\/s10836-007-5015-5","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9,21]]}}}