{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:51:46Z","timestamp":1743148306505,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[[2000]]},"DOI":"10.1007\/3-540-40922-x_9","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"145-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Combining Stream-Based and State-Based Verification Techniques"],"prefix":"10.1007","author":[{"given":"Nancy A.","family":"Day","sequence":"first","affiliation":[]},{"given":"Mark D.","family":"Aagaard","sequence":"additional","affiliation":[]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard and M. E. Leeser. Reasoning about pipelines with structural hazards. In Theorem Provers in Circuit Design (TPCD). pages 13\u201332, Springer, 1994.","DOI":"10.1007\/3-540-59047-1_40"},{"key":"9_CR2","unstructured":"S. Bainbridge, A. Camilleri, and R. Fleming. Theorem proving as an industrial tool for system level design. In Theorem Provers in Circuit Design (TPCD), pages 253\u2013274. Elsevier Science Publishers, 1992."},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"FMCAD","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In FMCAD, volume 1166 of LNCS, pages 187\u2013201. Springer, 1996."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"P. Bjesse, K. Claessen, M. Sheeran, and S. Singh. Lava: Hardware design in Haskell. In ACM Int. Conf. on Functional Programming (ICFP), pages 174\u2013184. ACM Press, 1998.","DOI":"10.1145\/291251.289440"},{"key":"9_CR5","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. V. Tassel. Experience with embedding hardware description languages in HOL. In Theorem Provers in Circuit Design (TPCD). pages 129\u2013156, Elsevier, 1992."},{"key":"9_CR6","unstructured":"J. R. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification (CAV)","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In Computer Aided Verification (CAV), volume 818 of LNCS, pages 68\u201380. Springer, 1994."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"K. Claessen and D. Sands. Observable sharing for functional circuit description. In Asian Computing Science Conference, 1999.","DOI":"10.1007\/3-540-46674-6_7"},{"key":"9_CR9","unstructured":"K. Claessen and M. Sheeran. A tutorial on Lava: A hardware description and verification system. April 9, 2000."},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR11","unstructured":"B. Cook, J. Launchbury, and J. Matthews. Specifying superscalar microprocessors in Hawk. In Workshop on Formal Techniques for Hardware, 1998."},{"key":"9_CR12","unstructured":"N. A. Day, J. Launchbury, and J. Lewis. Logical abstractions in Haskell. In Proceedings of the 1999 Haskell Workshop. Utrecht University Department of Computer Science, Technical Report UU-CS-1999-28, October 1999."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"M. Gordon. Reachability programming in Hol98 using BDDs. To appear in 13th International Conference on Theorem Proving and Higher Order Logics (TPHOLs), August, 2000.","DOI":"10.1007\/3-540-44659-1_12"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","DOI":"10.1109\/5.97300"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"S. D. Johnson, B. Bose, and C. D. Boyer. A tactical framework for digital design. In VLSI Specification, Verification and Synthesis, pages 349\u2013384. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_12"},{"key":"9_CR16","unstructured":"G. Jones and M. Sheeran. Circuit design in Ruby. In Formal Methods for VLSI Design, pages 13\u201370. Elsevier Science Publications, 1990."},{"key":"9_CR17","unstructured":"J. Matthews, B. Cook, and J. Launchbury. Microprocessor specification in Hawk. In International Conference on Computer Languages, 1998."},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/3-540-48683-6_26","volume-title":"Computer Aided Verification (CAV)","author":"J. Matthews","year":"1999","unstructured":"J. Matthews and J. Launchbury. Elementary microarchitecture algebra. In Computer Aided Verification (CAV), volume 1633 of LNCS, pages 288\u2013300. Springer, 1999."},{"key":"9_CR19","unstructured":"K. L. McMillan. SymbolicModel Checking. PhD thesis, Carnegie Mellon University, May 1992."},{"key":"9_CR20","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 481\u2013489. The British Computer Society, 1971."},{"key":"9_CR21","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989."},{"key":"9_CR22","unstructured":"J. C. Mitchell. Foundations for programming languages. MIT Press, 1996."},{"key":"9_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-15648-8_18","volume-title":"Logic of Programs","author":"J. C. Mitchell","year":"1985","unstructured":"J. C. Mitchell and A. R. Meyer. Second-order logical relations (extended abstract). In Logic of Programs, volume 193 of LNCS, pages 225\u2013236. Springer, 1985."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"J. O\u2019Donnell. Generating netlists from executable functional circuit specifications in a pure functional language. In Functional Programming Glasgow, Workshops in Computing, pages 178\u2013194. Springer, 1992","DOI":"10.1007\/978-1-4471-3215-8_16"},{"key":"9_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Concurrency and automata on in_nite sequences","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and automata on in_nite sequences. In 5th GI Conference on Theorectical Computer Science, volume 104 of LNCS. Springer, 1981."},{"key":"9_CR26","unstructured":"L. C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Lab, 1993. Latest edition: 24 November 1997."},{"key":"9_CR27","unstructured":"J. Peterson and K. Hammond, editors. Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.4). Yale University, Department of Computer Science, RR-1106, February 1997."},{"key":"9_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"Computer Aided Verification (CAV)","author":"J. Sawada","year":"1997","unstructured":"J. Sawada and W. Hunt. Trace table based approach for pipelined microprocessor verification. In Computer Aided Verification (CAV), volume 1254 of LNCS, pages 364\u2013375. Springer, 1997."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using transformations and verification in circuit design. In Designing Correct Circuits, 1992.","DOI":"10.1007\/978-1-4471-3558-6_12"},{"key":"9_CR30","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. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147\u2013189, March 1995.","journal-title":"Formal Methods in System Design"},{"key":"9_CR31","unstructured":"R. Sharp. T-Ruby: A tool for handing Ruby expressions. August, 1996."},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"S. Singh. Implementation of a nonstandard interpretation system. In Functional Programming, Glasgow, Workshops in Computing, pages 206\u2013224. Springer, 1989.","DOI":"10.1007\/978-1-4471-3166-3_14"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"P. Wadler. Theorems for free! In Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA89), pages 347\u2013359, 1989.","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T08:02:12Z","timestamp":1580284932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}