{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:26:50Z","timestamp":1775143610349,"version":"3.50.1"},"reference-count":34,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[1994,4,1]],"date-time":"1994-04-01T00:00:00Z","timestamp":765158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[1994,4]]},"DOI":"10.1109\/43.275352","type":"journal-article","created":{"date-parts":[[2002,8,24]],"date-time":"2002-08-24T17:57:42Z","timestamp":1030211862000},"page":"401-424","source":"Crossref","is-referenced-by-count":339,"title":["Symbolic model checking for sequential circuit verification"],"prefix":"10.1109","volume":"13","author":[{"given":"J.R.","family":"Burch","sequence":"first","affiliation":[]},{"given":"E.M.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"D.E.","family":"Long","sequence":"additional","affiliation":[]},{"given":"K.L.","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"D.L.","family":"Dill","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","year":"1984","journal-title":"TFM Manual"},{"key":"ref32","article-title":"A computational theory and implementation of sequential hardware equivalence","volume":"3","author":"pixley","year":"1990","journal-title":"Proc of the 1990 Workshop on Computer-Aided Verfication"},{"key":"ref31","article-title":"Formal verification of the Encore Gigamax cache consistency protocol","author":"mcmillan","year":"1991","journal-title":"Proc Int l Symp Shared Memory Multiprocessors"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/127601.127702","article-title":"Representing circuits more efficiently in symbolic model checking","author":"burch","year":"1991","journal-title":"28th ACM\/IEEE Design Automation Conference DAC"},{"key":"ref11","article-title":"Symbolic model checking with partitioned transition relations","author":"burch","year":"1991","journal-title":"Proc Int Conf Very Large Scale Integration"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114827"},{"key":"ref13","article-title":"Symbolic model checking: 10<superscript>20<\/superscript> states and beyond","author":"burch","year":"1990","journal-title":"Proc Fifth IEEE Symp Logic in Computer Science"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129861"},{"key":"ref16","article-title":"Synthesis of synchronization skeletons for branching time temporal logic","volume":"131","author":"clarke","year":"1981","journal-title":"Logic of Programs Workshop"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref18","article-title":"Verification of synchronous sequential machines based on symbolic execution","volume":"407","author":"coudert","year":"1989","journal-title":"Automatic Verification Methods for Finite State Systems International Workshop"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"ref28","article-title":"A synthesis method for self-timed VLSI circuits","author":"martin","year":"1987","journal-title":"Proc IEEE Int Conf Computer Design"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1990.114826"},{"key":"ref27","article-title":"The design of a self-timed circuit for distributed mutual exclusion","author":"martin","year":"1985","journal-title":"Proc Chapel Hill Conf VLSI"},{"key":"ref3","first-page":"759","article-title":"Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic","author":"bose","year":"1989","journal-title":"IMEC-IFIP Int Workshop on Appl Formal Methods for Correct VLSI Design"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676711"},{"key":"ref29","author":"mcmillan","year":"1992","journal-title":"Symbolic Model Checking An Approach to the State Explosion Problem"},{"key":"ref5","article-title":"An improved algorithm for automatic verification of finite state machines using temporal logic","author":"browne","year":"1986","journal-title":"Proc First Symp Logic in Computer Science"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1145\/127601.127701","article-title":"Formal hardware verification by symbolic ternary trajectory evaluation","author":"bryant","year":"1991","journal-title":"28th ACM\/IEEE Design Automation Conference DAC"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1989.63359"},{"key":"ref9","article-title":"Formal verification of digital circuits using symbolic ternary system models","volume":"3","author":"bryant","year":"1990","journal-title":"Computer-Aided Verification Proceedings of the 1990 Workshop DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1990.130210"},{"key":"ref20","article-title":"Verifying temporal properties of sequential machines without building their state diagrams","volume":"3","author":"coudert","year":"1990","journal-title":"Proc of the 1990 Workshop on Computer-Aided Verfication"},{"key":"ref22","author":"dill","year":"1988","journal-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits"},{"key":"ref21","article-title":"Trace theory for automatic hierarchical verification of speed-independent circuits","author":"dill","year":"1988","journal-title":"Advanced Research in VLSI Proc Fifth MIT Conf"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-89208-9.50020-X"},{"key":"ref23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","author":"dill","year":"1989","journal-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129940"},{"key":"ref25","author":"kurshan","year":"1986","journal-title":"Testing containment of ?-regular languages"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx1\/43\/6821\/00275352.pdf?arnumber=275352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:11:24Z","timestamp":1638216684000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/275352\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,4]]},"references-count":34,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/43.275352","relation":{},"ISSN":["0278-0070"],"issn-type":[{"value":"0278-0070","type":"print"}],"subject":[],"published":{"date-parts":[[1994,4]]}}}