{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:54Z","timestamp":1725663894983},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_61","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:19Z","timestamp":1330269919000},"page":"273-285","source":"Crossref","is-referenced-by-count":0,"title":["Composing symbolic trajectory evaluation results"],"prefix":"10.1007","author":[{"given":"Scott","family":"Hazelhurst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carl-Johan H.","family":"Seger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"20","author":"R. E. Bryant","year":"1991","unstructured":"R. E. Bryant. On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Transactions on Computers, 20(2):205\u2013213, Feb. 1991.","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"23_CR2","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24(3):293\u2013318, Sept. 1992.","journal-title":"ACM Computing Surveys"},{"key":"23_CR3","volume-title":"Compositional Model Checking","author":"E. Clarke","year":"1989","unstructured":"E. Clarke, D. Long, and K. McMillan. Compositional Model Checking. In IEEE Fourth Annual Symposium on Logic in Computer Science, Washington, D.C., 1989. IEEE Computer Society."},{"volume-title":"Lecture Notes in Computer Science 697","year":"1993","key":"23_CR4","unstructured":"C. Courcoubetis, editor. Proceedings of the 5th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science 697, Berlin, July 1993. Springer-Verlag."},{"key":"23_CR5","unstructured":"S. Hazelhurst and C.-J. H. Seger. A Simple Theorem Prover Based on Symbolic Trajectory Evaluation and OBDDs. Technical Report 93-41, Department of Computer Science, University of British Columbia, Nov. 1993. Available by anonymous ftp as ftp.cs.ubc.ca:\/pub\/local\/techreports\/1993\/TR-93-41.ps.gz."},{"key":"23_CR6","first-page":"154","volume-title":"Lecture Notes in Computer Science 697","author":"H. Hungar","year":"1993","unstructured":"H. Hungar. Combining Model Checking and Theorem Proving to Verify Parallel Processes. In Courcoubetis [4], pages 154\u2013165."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"J. J. Joyce and C.-J. H. Seger. Linking BDD-based Symbolic Evaluation to Interactive Theorem-Proving. In Proceedings of the 30th Design Automation Conference. IEEE Computer Society Press, June 1993.","DOI":"10.1145\/157485.164981"},{"key":"23_CR8","first-page":"166","volume-title":"Lecture Notes in Computer Science 697","author":"R. Kurshan","year":"1993","unstructured":"R. Kurshan and L. Lamport. Verification of a Multiplier: 64 Bits and Beyond. In Courcoubetis [4], pages 166\u2013179."},{"key":"23_CR9","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, School of Computer Science, July 1993. Technical report CMU-CS-93-178."},{"issue":"5","key":"23_CR10","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1109\/43.277609","volume":"12","author":"M. C. McFarland","year":"1993","unstructured":"M. C. McFarland. Formal Verification of Sequential Hardware: A Tutorial. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(5):633\u2013654, May 1993.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"23_CR11","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, London, 1989."},{"key":"23_CR12","unstructured":"C.-J. H. Seger and R. E. Bryant. Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Technical Report 93-8, Department of Computer Science, University of British Columbia, Apr. 1993."},{"key":"23_CR13","unstructured":"C.-J. H. Seger and J. J. Joyce. A Mathematically Precise Two-Level Hardware Verification Methodology. Technical Report 92\u201334, Department of Computer Science, University of British Columbia, Dec. 1992."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_61.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:12:02Z","timestamp":1619572322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_61"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_61","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}