{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:40:25Z","timestamp":1742600425434,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603856"},{"type":"electronic","value":"9783540455165"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"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":[[1995]]},"DOI":"10.1007\/3-540-60385-9_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:24:36Z","timestamp":1330280676000},"page":"103-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic analysis and verification of CPA descriptions"],"prefix":"10.1007","author":[{"given":"M. C.","family":"McFarland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. J.","family":"Kowalski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1109\/TC.1982.1675978","volume":"C-31","author":"G. V. Bochmann","year":"1982","unstructured":"Bochmann, G. V., \u201cHardware Specification with Temporal Logic: An Example,\u201d IEEE Transactions on Computers C-31(3), pp. 223\u2013231 (March, 1982).","journal-title":"IEEE Transactions on Computers"},{"issue":"12","key":"7_CR2","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"M. C. Browne","year":"1986","unstructured":"Browne, M. C., Clarke, E. M., Dill, D. L., and Mishra, B., \u201cAutomatic Verification of Sequential Circuits Using Temporal Logic,\u201d IEEE Transactions on Computers C-35(12), pp. 1035\u20131044 (December, 1986).","journal-title":"IEEE Transactions on Computers"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Darringer, J., \u201cThe application of program verification techniques to hardware verification,\u201d Proceedings of the Sixteenth Design Automation Conference, pp. 375\u2013381, ACM SIGDA and IEEE Computer Society DATC (June, 1979).","DOI":"10.1109\/DAC.1979.1600139"},{"key":"7_CR4","volume-title":"UCLA-ENG-7784","author":"S. Crocker","year":"1978","unstructured":"Crocker, S., \u201cState deltas: A formalism for representing segments of computation,\u201d UCLA-ENG-7784, Computer Science Department, University of California at Los Angeles (February, 1978)."},{"key":"7_CR5","volume-title":"PhD Thesis","author":"W. A. Hunt","year":"1986","unstructured":"Hunt, W. A., FM8501: A Verified Microprocessor, PhD Thesis, University of Texas at Austin (February, 1986)."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Devadas, S., Ma, H. T., and Newton, A. R., \u201cOn The Verification of Sequential Machines At Different Levels of Abstraction,\u201d Proceedings of the 24th Design Automation Conference, pp. 271\u2013276, ACM\/IEEE (June, 1987).","DOI":"10.1145\/37888.37929"},{"issue":"11","key":"7_CR7","doi-asserted-by":"crossref","first-page":"1356","DOI":"10.1109\/43.97615","volume":"10","author":"R. P. Kurshan","year":"1991","unstructured":"Kurshan, R. P. and McMillan, K. L., \u201cAnalysis of Digital Circuits Through Symbolic Reduction,\u201d IEEE Transactions on Computer-Aided Design 10(11), pp. 1356\u20131371 (November, 1991).","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"7_CR8","unstructured":"Berthet, C., Coudert, O., and Madre, J., \u201cNew Ideas on Symbolic Manipulations of Finite State Machines,\u201d International Conference on Computer Design, IEEE (September, 1990)."},{"issue":"8","key":"7_CR9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R., \u201cGraph-Based Algorithms for Boolean Function Manipulation,\u201d IEEE Transactions on Computers C-35(8), pp. 677\u2013691 (August, 1986).","journal-title":"IEEE Transactions on Computers"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Burch, J. R., Clarke, E. M., and Long, D. E., \u201cRepresenting Circuits More Efficiently in Symbolic Model Checking,\u201d Proceedings of the 28th Design Automation Conference, pp. 403\u2013407, ACM\/IEEE (June, 1991).","DOI":"10.1145\/127601.127702"},{"key":"7_CR11","volume-title":"Formal Aspects of VLSI Design","author":"M. Gordon","year":"1986","unstructured":"Gordon, M., \u201cWhy higher-order logic is a good formalism for specifying and verifying hardware,\u201d in Formal Aspects of VLSI Design, Milne, G. and Subrahmanyam, P. A. (Eds.), North Holland, New York (1986)."},{"issue":"2","key":"7_CR12","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/360827.360850","volume":"17","author":"B. Wegbreit","year":"1974","unstructured":"Wegbreit, B., \u201cThe synthesis of loop predicates,\u201d Communications of the ACM 17(2), pp. 102\u2013112 (February, 1974).","journal-title":"Communications of the ACM"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Devadas, S., Keutzer, K., and Krishnakumar, A. S., \u201cDesign Verification and Reachability Analysis Using Algebraic Manipulation,\u201d Proceedings of the International Conference on Computer Design, pp. 250\u2013258, IEEE (October, 1991).","DOI":"10.1109\/ICCD.1991.139892"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Lee, D. and Yannakakis, M., \u201cOnline Minimization of Transition Systems,\u201d Proceedings of the 24th Annual ACM Symposium on the Theory of Computing, pp. 264\u2013274, ACM (May, 1992).","DOI":"10.1145\/129712.129738"},{"key":"7_CR15","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, J., \u201cSymbolic Model Checking 10\u222720 States and Beyond,\u201d Proceedings of the Fifth Annual Symposium on Logic in Computer Science (June, 1990)."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"McFarland, M. C. and Kowalski, T. J., \u201cSpecifying System Behavior in CPA,\u201d ICCD91, pp. 342\u2013345, IEEE (October, 1991).","DOI":"10.1109\/ICCD.1991.139914"},{"key":"7_CR17","unstructured":"Chu, T., Synthesis of Self-timed VLSI Circuits from Graph-Theoretic Specifications, PhD Thesis, Department of Electrical Engineering and Computer Science, MIT (May, 1987)."},{"key":"7_CR18","volume-title":"CPA: Giving an Account of Timed System Behavior","author":"M. C. McFarland","year":"1990","unstructured":"McFarland, M. C., \u201cCPA: Giving an Account of Timed System Behavior,\u201d ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU'90), ACM, Vancouver, BC (August, 1990)."},{"key":"7_CR19","volume-title":"Language and Formal Semantics of the Specification System CPA","author":"M. C. McFarland","year":"1992","unstructured":"McFarland, M. C., Kowalski, T. J., and Peman, M. J., \u201cLanguage and Formal Semantics of the Specification System CPA,\u201d Proceedings of the International Workshop on Hardware-Software Co-design, IEEE, Estest Park, CO (September 30, 1992)."},{"issue":"11","key":"7_CR20","doi-asserted-by":"crossref","first-page":"1331","DOI":"10.1109\/T-C.1971.223135","volume":"C-20","author":"J. C. King","year":"1971","unstructured":"King, J. C., \u201cProving programs to be correct,\u201d IEEE Transactions on Computers C-20(11), pp. 1331\u20131336 (November, 1971).","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"7_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/32.21720","volume":"15","author":"D. Sarkar","year":"1989","unstructured":"Sarkar, D. and De Sarkar, S. C., \u201cSome Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers,\u201d IEEE Transactions on Software Engineering 15(1), pp. 1\u20138 (January, 1989).","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR22","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1991","unstructured":"Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications, McGraw-Hill, New York (1991)."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60385-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:02:19Z","timestamp":1742598139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"2 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}