{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:48:04Z","timestamp":1754488084645,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[[1997]]},"DOI":"10.1007\/3-540-63166-6_37","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:14:16Z","timestamp":1330298056000},"page":"376-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["On combining formal and informal verification"],"prefix":"10.1007","author":[{"given":"Jun","family":"Yuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Shen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"37_CR1","unstructured":"P. Ashar and S. Malik. Fast Functional Simulation Using Branching Programs. In Proc. Intl. Conf. on Computer-Aided Design, November 1995."},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for Verification and Synthesis. In Proc. of the Computer Aided Verification Conf., July 1996.","DOI":"10.1007\/3-540-61474-5_95"},{"key":"37_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35:677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"B. Chen, M. Yamazaki, and M. Fujita. Bug Identification of a Real Chip Design by Symbolic Model Checking. In Proc. European Conf. on Design Automation, pages 132\u2013136, March 1994.","DOI":"10.1109\/EDTC.1994.326886"},{"key":"37_CR5","unstructured":"H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi. A Structural Approach to State Space Decomposition for Approximate Reachability Analysis. In Proc. Intl. Conf. on Computer Design, October 1994."},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"W.J. Culler. Implementing Safety Critical Systems: The VIPER microprocessor. Kluwer Academic Publishment, 1987.","DOI":"10.1007\/978-1-4613-2007-4_1"},{"key":"37_CR7","unstructured":"Richard C. Ho, C. Han Yang, Mark A. Horowitz, and David L. Dill. Architectural Validation for Processors. In Proceedings of the International Symposium on Computer Architecture, June 1995."},{"key":"37_CR8","unstructured":"Y. Hoskote, D. Moundanos, and J. Abraham. Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. In Proc. Intl. Conf. on Computer Design, Austin, TX, October 1995."},{"key":"37_CR9","unstructured":"B. Lin and R. Newton. Implicit Manipulation of Equivalence Classes Using Binary Decision Diagrams. In Proc. Intl. Conf. on Computer Design, Cambridge, MA, October 1991."},{"key":"37_CR10","unstructured":"P. McGeer, K. McMillan, A. Saldanha, A. Sangiovanni-Vincentelli, and P. Scaglia. Fast Discrete Function Evaluation. In Proc. Intl. Conf. on Computer-Aided Design, November 1995."},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"R. Ranjan, J. Sanghavi, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. High Performance BDD Package Based on Exploiting Memory Hierarchy. In Proc. of the Design Automation Conf., Las Vegas, NV, June 1996.","DOI":"10.1145\/240518.240638"},{"key":"37_CR13","unstructured":"K. Ravi and F. Somenzi. High Density Reachability Analysis. In Proc. Intl. Conf. on Computer-Aided Design, Santa Clara, CA, November 1995."},{"key":"37_CR14","volume-title":"PhD thesis","author":"V. Singhal","year":"1996","unstructured":"Vigyan Singhal. Design Replacements for Sequential Circuits. PhD thesis, University of California Berkeley, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720, 1996."},{"issue":"3","key":"37_CR15","first-page":"131","volume":"9","author":"K. Thompson","year":"1986","unstructured":"K. Thompson. Retrograde analysis of certain endgames. ICCA Journal, 9(3):131\u2013139, 1986.","journal-title":"ICCA Journal"}],"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-63166-6_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:39:14Z","timestamp":1742600354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}