{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215619,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_36","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"418-430","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Model Checking Based on Sequential ATPG"],"prefix":"10.1007","author":[{"given":"Vamsi","family":"Boppana","sequence":"first","affiliation":[]},{"given":"Sreeranga P.","family":"Rajan","sequence":"additional","affiliation":[]},{"given":"Koichiro","family":"Takayama","sequence":"additional","affiliation":[]},{"given":"Masahiro","family":"Fujita","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"36_CR1","volume-title":"Digital System Testing and Testable Design","author":"M. Abramovici","year":"1990","unstructured":"M. Abramovici, M. A. Breuer, and A. D. Friedman. Digital System Testing and Testable Design. NewYork, NY: Computer Science Press, 1990."},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and T. A. Henzinger, editors. Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July\/August 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61474-5"},{"key":"36_CR3","unstructured":"V. Boppana. State information-based solutions for sequential circuit diagnosis and testing. Technical Report CRHC-97-20, Ph.D. thesis, Center for Reliable and High-Performance Computing, University of Illinois at Urbana-Champaign, July 1997."},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In Proceedings of the International Conference on Computer-Aided Design, pages 236\u2013243, November 1995.","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"K. T. Cheng and V. Agrawal. State Assignment for Initialilzable Synthesis. In Proc. Intl. Conf. Computer-Aided Design, pages 212\u2013215, November 1989.","DOI":"10.1109\/ICCAD.1989.76938"},{"issue":"3","key":"36_CR6","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1109\/12.127453","volume":"41","author":"K. T. Cheng","year":"1993","unstructured":"K. T. Cheng and V. Agrawal. Initializability consideration in sequential machine synthesis. IEEE Trans. Computers, 41(3):374\u2013379, March 1993.","journal-title":"IEEE Trans. Computers"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of concurrency-Reflections and Perspectives, volume 803 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58043-3_19"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"K. T. Cheng and H. K. T. Ma. On the over-specification problem in sequentialATPG algorithms. In Proc. Design Automation Conf., pages 16\u201321, June 1992.","DOI":"10.1109\/DAC.1992.227870"},{"issue":"10","key":"36_CR9","doi-asserted-by":"publisher","first-page":"1599","DOI":"10.1109\/43.256935","volume":"12","author":"K. T. Cheng","year":"1993","unstructured":"K. T. Cheng and H. K. T. Ma. On the over-specification problem in sequentialATPG algorithms. IEEE Trans. Computer-Aided Design, 12(10):1599\u20131604, October 1993.","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"36_CR10","unstructured":"M. Fujita, H. Tanaka, and T. Moto-oka. Verification with prolog and temporal logic. In Proc. of IFIP WG10.2 International Conference on Hardware Description Languages and their Applications, May 1983."},{"key":"36_CR11","unstructured":"M. Fujita, H. Tanaka, and T. Moto-oka. Logic design assistance with temporal logic. In Proc. of IFIP WG10.2 International Conference on Hardware Description Languages and their Applications, Aug. 1985."},{"issue":"3","key":"36_CR12","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TC.1981.1675757","volume":"C-30","author":"P. Goel","year":"1990","unstructured":"P. Goel. An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans. Computers, C-30(3):215\u2013222, March 1990.","journal-title":"IEEE Trans. Computers"},{"key":"36_CR13","unstructured":"The VIS Group. VIS:A system for verification and synthesis. In Alur and Henzinger [AH96], pages 428\u2013432."},{"key":"36_CR14","volume-title":"Finite-State Models for Logical Machines","author":"F. C. Hennie","year":"1968","unstructured":"F. C. Hennie. Finite-State Models for Logical Machines. NewYork, NY: JohnWiley & Sons, Inc., 1968."},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"M. S. Hsiao, E. M. Rudnick, and J. H. Patel. Sequential circuit test generation using dynamic state traversal. In Proc. European Design and Test Conf., pages 22\u201328, March 1997.","DOI":"10.1109\/EDTC.1997.582325"},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"H. Iwashita and T. Nakata. Forward model checking techniques oriented to buggy designs. In Proc. Intl. Conf. Computer-Aided Design, pages 400\u2013404, November 1997.","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"H. Iwashita, T. Nakata, and F. Hirose. Ctl model checking based on forward state traversal. In Proc. Intl. Conf. Computer-Aided Design, pages 82\u201387, November 1996.","DOI":"10.1109\/ICCAD.1996.569084"},{"key":"36_CR18","volume-title":"Switching and Finite Automata Theory","author":"Z. Kohavi","year":"1978","unstructured":"Z. Kohavi. Switching and Finite Automata Theory. New York, NY: McGraw-Hill, 1978."},{"key":"36_CR19","volume-title":"Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach","author":"R. P. Kurshan","year":"1994","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach. Princeton University Press, Princeton, NJ, 1994."},{"key":"36_CR20","doi-asserted-by":"crossref","unstructured":"O. Kupferman and MosheY. Vardi. Model checking of safety properties. In CAV99, 1999.","DOI":"10.1007\/3-540-48683-6_17"},{"key":"36_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Pub., Boston, MA, 1993."},{"key":"36_CR22","unstructured":"H. Nakamura, M. Fujita, S. Kono, and H. Tanaka. Temporal logic based fast verification systems using cover expressions. In Proc. of IFIP WG10.5 International Conference on VLSI, Aug. 1987."},{"key":"36_CR23","doi-asserted-by":"crossref","unstructured":"T. Niermann and J. H. Patel. HITEC:A test generation package for sequential circuits. In Proc. European Design Automation Conf., pages 214\u2013218, February 1991.","DOI":"10.1109\/EDAC.1991.206393"},{"key":"36_CR24","doi-asserted-by":"crossref","unstructured":"[ORR+96]_ S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Alur and Henzinger [AH96], pages 411\u2013414.","DOI":"10.1007\/3-540-61474-5_91"},{"issue":"1","key":"36_CR25","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"Doron Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design, 8(1):39\u201364, 1996.","journal-title":"Formal Methods in System Design"},{"issue":"5","key":"36_CR26","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1109\/12.142689","volume":"40","author":"I. Pomeranz","year":"1992","unstructured":"I. Pomeranz and S. M. Reddy. The multiple observation time test strategy. IEEE Trans. Computer-Aided Design, 40(5):627\u2013637, May 1992.","journal-title":"IEEE Trans. Computer-Aided Design"},{"issue":"9","key":"36_CR27","doi-asserted-by":"publisher","first-page":"1066","DOI":"10.1109\/12.241596","volume":"42","author":"I. Pomeranz","year":"1993","unstructured":"I. Pomeranz and S. M. Reddy. Classification of faults in synchronous sequential circuits. IEEE Trans. Computers, 42(9):1066\u20131077, September 1993.","journal-title":"IEEE Trans. Computers"},{"key":"36_CR28","doi-asserted-by":"crossref","unstructured":"K. Takayama, T. Satoh, T. Nakata, and F. Hirose. An approach to verify a large scale system-on-a-chip using symbolic model checking. In Proceedings of the International Conference on Computer Design, pages 308\u2013313, October 1998.","DOI":"10.1109\/ICCD.1998.727066"},{"key":"36_CR29","unstructured":"P. Wolper. \u201csynthesis of communicating processes from temporal logic specifications\u201d. Technical Report STAN-CS-82-925, Dept. of Computer Science, Stanford University, 1982."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T12:37:37Z","timestamp":1737463057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}