{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:46Z","timestamp":1755217786434,"version":"3.43.0"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1023\/a:1022977607142","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"163-173","source":"Crossref","is-referenced-by-count":0,"title":["Verisym: Verifying Circuits by Symbolic Simulation"],"prefix":"10.1007","volume":"22","author":[{"given":"William","family":"Adams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damir","family":"Jamsek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5117032_CR1","unstructured":"B.C. Brock, W.A. Hunt, Jr., and W.D. Young, \u201cAn introduction to a formally-defined hardware description language,\u201d Technical Report 76, Computational Logic Incorporated, 1992."},{"issue":"8","key":"5117032_CR2","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"5117032_CR3","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1109\/TCAD.1987.1270309","volume":"CAD-6","author":"R.E. Bryant","year":"1987","unstructured":"R.E. Bryant, \u201cAlgorithmic aspects of symbolic switch network analysis,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. CAD-6, No. 4, pp. 618\u2013633, 1987a.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"4","key":"5117032_CR4","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1109\/TCAD.1987.1270310","volume":"CAD-6","author":"R.E. Bryant","year":"1987","unstructured":"R.E. Bryant, \u201cBoolean analysis of MOS circuits,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. CAD-6, No. 4, pp. 634\u2013649, 1987b.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5117032_CR5","unstructured":"R.E. Bryant, Private communication, 2001."},{"key":"5117032_CR6","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler, \u201cCOSMOS: A compiled simulator for MOS circuits,\u201d in Proceedings of the 24th Design Automation Conference, 1987, pp. 9\u201316.","DOI":"10.1145\/37888.37890"},{"key":"5117032_CR7","unstructured":"S.C. Kleene, Introduction to Metamathematics, North-Holland, Amsterdam, 1952."},{"issue":"1\/2","key":"5117032_CR8","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1147\/rd.391.0149","volume":"39","author":"A. Kuehlman","year":"1995","unstructured":"A. Kuehlman, A. Srinivasan, and D.P. LaPotin, \u201cVerity: A formal verification program for custom CMOS circuits,\u201d IBM Journal of Research and Development, Vol. 39, No. 1\/2, pp. 149\u2013166, 1995.","journal-title":"IBM Journal of Research and Development"},{"key":"5117032_CR9","unstructured":"A. Martin, \u201cPrinciples and practice of symbolic trajectory evaluation,\u201d in Tutorial Presentation at the 13th International Conference on Theorem Proving in Higher-Order Logics, 2000."},{"key":"5117032_CR10","unstructured":"L.W. Nagel, \u201cSPICE2: A computer program to simulate semiconductor circuits,\u201d Memorandum ERL-M520, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, 1975."},{"key":"5117032_CR11","volume-title":"Tcl and the Tk Toolkit","author":"J.K. Ousterhout","year":"1994","unstructured":"J.K. Ousterhout, Tcl and the Tk Toolkit, Addison-Wesley, Reading, MA, 1994."},{"key":"5117032_CR12","unstructured":"M. Pandey, \u201cFormal verification of memory arrays,\u201d Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University. Available as Technical Report CMU-CS\u201397\u2013162, 1997."},{"issue":"2","key":"5117032_CR13","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"C.-J.H. Seger and R.E. Bryant, \u201cFormal verification by symbolic evaluation of partially-ordered trajectories,\u201d Formal Methods in System Design, Vol. 6, No. 2, pp. 147\u2013190, 1995.","journal-title":"Formal Methods in System Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022977607142.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022977607142\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022977607142.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:21:37Z","timestamp":1754421697000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022977607142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["5117032"],"URL":"https:\/\/doi.org\/10.1023\/a:1022977607142","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}