{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T09:17:06Z","timestamp":1672478226804},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1994,2,1]],"date-time":"1994-02-01T00:00:00Z","timestamp":760060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,2]]},"DOI":"10.1007\/bf01384079","type":"journal-article","created":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T22:30:17Z","timestamp":1112394617000},"page":"83-97","source":"Crossref","is-referenced-by-count":8,"title":["Verifying the summit bus converter protocols with symbolic model checking"],"prefix":"10.1007","volume":"4","author":[{"given":"Cheryl","family":"Harkness","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elizabeth","family":"Wolf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"CR1","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"35","author":"M.C. Browne","year":"1986","unstructured":"M.C. Browne, E.M. Clarke, D.L. Dill, and B. Mishra, Automatic verification of sequential circuits using temporal logic.IEEE Transactions on Computers C35(12): 1035?1044, December 1986.","journal-title":"IEEE Transactions on Computers C"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/123186.123223","volume-title":"27th ACM\/IEEE Design Automation Conference","author":"J.R. Burch","year":"1990","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking. In27th ACM\/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, pp. 46?51, June 1990."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1109\/LICS.1990.113767","volume-title":"Fifth Annual IEEE Symposium on Logic in Computer Science","author":"J.R. Burch","year":"1990","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. InFifth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos CA, June 1990, pp. 428?439."},{"issue":"2","key":"CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic.ACM Transactions on Programming Languages and Systems, 8(2): 244?263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR5","unstructured":"Acme Bus Converter External Reference Specification. Hewlett-Packard, Mainline Systems Lab, Cupertino, CA, May 1991, internal document."},{"key":"CR6","unstructured":"SUMMIT Bus Converter External Reference Specification. Hewlett-Packard, Mainline Systems Lab, Cupertino, CA, August 1990, internal document."},{"key":"CR7","unstructured":"K.L. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistency protocol. InInternational Symposium on Shared Memory Multiprocessors, pp. 242?251, 1991."},{"issue":"8","key":"CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, Graph-based algorithms for boolean function manipulation.IEEE Transactions on Computers, C35(8): 677?691, August 1986.","journal-title":"IEEE Transactions on Computers, C"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384079\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T12:04:49Z","timestamp":1556798689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,2]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,2]]}},"alternative-id":["BF01384079"],"URL":"https:\/\/doi.org\/10.1007\/bf01384079","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,2]]}}}