{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,10,29]],"date-time":"2022-10-29T05:50:57Z","timestamp":1667022657229},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2004,4,27]],"date-time":"2004-04-27T00:00:00Z","timestamp":1083024000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,8]]},"DOI":"10.1007\/s10009-004-0142-0","type":"journal-article","created":{"date-parts":[[2004,4,26]],"date-time":"2004-04-26T05:12:39Z","timestamp":1082956359000},"page":"174-182","source":"Crossref","is-referenced-by-count":1,"title":["Test sequence generation and model checking using dynamic transition relations"],"prefix":"10.1007","volume":"6","author":[{"given":"S\u00e9rgio","family":"Campos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karen","family":"Yorav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Copty","family":"Fady","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,27]]},"reference":[{"key":"142_CR1","unstructured":"Beenker F, Dekker R, Stans R, van der Star M (1989) A testability strategy for silicon computers. In: Proceedings of the international test conference, Washington, DC, August 1989, pp 660\u2013669"},{"key":"142_CR2","doi-asserted-by":"crossref","unstructured":"Boppana V, Rajan S, Takayama K, Fujita M (1999) Model checking based on sequential ATPG. In: Proceedings of the conference on computer aided verification, Trento, Italy, July 1999, pp 418\u2013430","DOI":"10.1007\/3-540-48683-6_36"},{"key":"142_CR3","doi-asserted-by":"crossref","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691","DOI":"10.1109\/TC.1986.1676819"},{"key":"142_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"142_CR5","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1023\/A:1008713601998","volume":"17","author":"Campos","year":"2000","unstructured":"Campos S, Clarke E, Grumberg O (2000) Selective quantitative analysis and interval model checking: verifying different facets of a system. Formal Meth Sys Des 17:163\u2013192","journal-title":"Formal Meth Sys Des"},{"key":"142_CR6","doi-asserted-by":"crossref","unstructured":"Campos S, Clarke E, Marrero W, Minea M (1995) Verifying the performance of the PCI local bus using symbolic techniques. In: Proceedings of the international conference on computer design, Austin, TX, October 1995, pp 72\u201378","DOI":"10.1109\/ICCD.1995.528793"},{"key":"142_CR7","doi-asserted-by":"crossref","unstructured":"Chakrabarty K, Murray B, Iyengar V (1999) Built-in test pattern generation for high-performance circuits using twisted-ring counters. In: Proceedings of the IEEE VLSI Test symposium, San Diego, 22\u201327 April 1999","DOI":"10.1109\/VTEST.1999.766642"},{"key":"142_CR8","unstructured":"Clarke E, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge, MA"},{"key":"142_CR9","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Programm Lang Sys 8(2):244\u2013263","journal-title":"ACM Trans Programm Lang Sys"},{"key":"142_CR10","unstructured":"Coudert O, Madre JC, Berthet C (1990) Verifying temporal properties of sequential machines without building their state diagrams. In: Proceedings of the conference on computer aided verification, Grenoble, France, pp 365\u2013373"},{"key":"142_CR11","doi-asserted-by":"crossref","unstructured":"Engels A, Feijs L, Mauw S (1997) Test generation for intelligent networks using model checking. In: Proceedings of the 3rd conference on tools and algorithms for the construction and analysis of systems (TACAS), Enschede, The Netherlands, April 1997, pp 384\u2013398","DOI":"10.1007\/BFb0035401"},{"key":"142_CR12","doi-asserted-by":"crossref","unstructured":"Fernandez JC, Jard C, Jeron T, Viho C (1996) Using on-the-fly verification techniques for the generation of test suites. In: Proceedings of the conference on computer aided verification, New Brunswick, NJ, August 1996","DOI":"10.1007\/3-540-61474-5_82"},{"key":"142_CR13","unstructured":"Goga N (2000) An optimization of the TorX test generation algorithm. Xootic Mag November 2000, pp 15\u201321"},{"key":"142_CR14","doi-asserted-by":"crossref","unstructured":"Lee J, Patel JH (1991) An architectural level test generator for a hierarchical design environment. In: Proceedings of the 21st symposium on fault-tolerant computing, Nashville, TN, October 1991, pp 729\u2013738","DOI":"10.1109\/FTCS.1991.146631"},{"key":"142_CR15","doi-asserted-by":"crossref","unstructured":"Lee J, Patel JH (1993) An architectural level test generator for a hierarchical design environment based on nonlinear equation solving. J Electron Test","DOI":"10.1007\/BF00971643"},{"key":"142_CR16","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Dordrecht","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"142_CR17","unstructured":"Murray B (1994) Hierarchical testing using precomputed tests for modules. PhD thesis, Department of Computer Science and Engineering, University of Michigan, Ann Arbor, MI"},{"key":"142_CR18","doi-asserted-by":"crossref","unstructured":"Petrenko A, Yevtushenko N, Bochmann G (1996) Testing deterministic implementations from nondeterministic FSM specifications. In: Proceedings of the 9th international workshop on protocol test systems, Darmstadt, Germany, pp 125\u2013140","DOI":"10.1007\/978-0-387-35062-2_10"},{"key":"142_CR19","unstructured":"Tretmans J, Belinfante A (1999) Automatic testing with formal methods. In: Proceedings of EuroSTAR\u201999: 7th European international conference on software testing, analysis and review, Barcelona, Spain, November 1999"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0142-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0142-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0142-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:18Z","timestamp":1559100318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0142-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,27]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["142"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0142-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,27]]}}}