{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:41:46Z","timestamp":1742913706645,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_23","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"341-358","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Symbolic Functional Evaluation"],"prefix":"10.1007","author":[{"given":"Nancy A.","family":"Day","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey J.","family":"Joyce","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, M. E. Leeser, and P. J. Windley. Towards a super duper hardware tactic. In J. J. Joyce and C.-J. H. Seger, editors, HOL User\u2019s Group Workshop. Springer-Verlag, August 1993.","DOI":"10.1007\/3-540-57826-9_151"},{"key":"23_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/BFb0028383","volume-title":"TPHOLs","author":"J. H. Andrews","year":"1997","unstructured":"J. H. Andrews. Executing formal specifications by translating to higher order logic programming. In TPHOLs, volume 1275 of LNCS, pages 17\u201332. Springer Verlag, 1997."},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"J. H. Andrews, N. A. Day, and J. J. Joyce. Using a formal description technique to model aspects of a global air traffic telecommunications network. In FORTE\/PSTV\u201997, 1997.","DOI":"10.1007\/978-0-387-35271-8_26"},{"issue":"1","key":"23_CR4","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"J. M. Atlee","year":"1993","unstructured":"J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Trans. on Soft. Eng., 19(1):24\u201340, January 1993.","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"23_CR5","unstructured":"R. Bharadwaj and C. Heitmeyer. Verifying SCR requirements specifications using state space exploration. In Proceedings of the First ACM SIGPLAN Workshop on Automatic Analysis of Software, 1997."},{"key":"23_CR6","unstructured":"R. Boulton et al. Experience with embedding hardware description languages in HOL. In Theorem Provers in Circuit Design, pages 129\u2013156. North-Holland, 1992."},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/321864.321875","volume":"72","author":"R. S. Boyer","year":"1975","unstructured":"R. S. Boyer and J. S. Moore. Proving theorems about LISP functions. Jour. of the ACM, 72(1):129\u2013144, January 1975.","journal-title":"Jour. of the ACM"},{"issue":"8","key":"23_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"23_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"CAV","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In CAV, volume 818 of LNCS, pages 68\u201379. Springer-Verlag, 1994."},{"key":"23_CR10","unstructured":"A. J. Camilleri. Simulation as an aid to verification using the HOL theorem prover. Technical Report 150, University of Cambridge Computer Laboratory, October 1988."},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00243000","volume":"5","author":"A. Cohn","year":"1989","unstructured":"A. Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127\u2013139, June 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"C. Consel and O. Danvy. Tutorial notes on partial evaluation. In POPL, pages 493\u2013501. ACM Press, 1993.","DOI":"10.1145\/158511.158707"},{"key":"23_CR13","first-page":"338","volume":"78","author":"N. Day","year":"1993","unstructured":"N. Day and J. Joyce. The semantics of statecharts in HOL. In HOL User\u2019s Group Workshop, volume 78, pages 338\u2013351. Springer-Verlag, 1993.","journal-title":"HOL User\u2019s Group Workshop"},{"key":"23_CR14","unstructured":"N. A. Day. A Framework for Multi-Notation, Model-Oriented Requirements Analysis. PhD thesis, Department of Computer Science, University of British Columbia, 1998."},{"key":"23_CR15","unstructured":"N. A. Day, J. J. Joyce, and G. Pelletier. Formalization and analysis of the separation minima for aircraft in the North Atlantic Region. In Fourth NASA Langley Formal Methods Workshop, pages 35\u201349. NASA Conference Publication 3356, September 1997."},{"key":"23_CR16","unstructured":"N. A. Day, J. R. Lewis, and B. Cook. Symbolic simulation of microprocessor models using type classes in Haskell. To appear in CHARME\u201999 poster session."},{"key":"23_CR17","unstructured":"M. Gordon and T. Melham, editors. Introduction to HOL. Cambridge University Press, 1993."},{"key":"23_CR18","unstructured":"M. J. C. Gordon. Combining deductive theorem proving with symbolic state enumeration. Transparencies from a presentation, summer 1998."},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, pages 387\u2013439. Springer-Verlag, 1988.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"23_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/3-540-49519-3_21","volume-title":"FMCAD","author":"D. A. Greve","year":"1998","unstructured":"D. A. Greve. Symbolic simulation of the JEM1 microprocessor. In FMCAD, volume 1522 of LNCS, pages 321\u2013333. Springer, 1998."},{"key":"23_CR21","first-page":"231","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computing, 8:231\u2013274, 1987.","journal-title":"Science of Computing"},{"issue":"6","key":"23_CR22","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/32.508311","volume":"22","author":"M. P. Heimdahl","year":"1996","unstructured":"M. P. Heimdahl and N. G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Trans. on Soft. Eng., 22(6):363\u2013377, June 1996.","journal-title":"IEEE Trans. on Soft. Eng."},{"issue":"3","key":"23_CR23","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C. L. Heitmeyer","year":"1996","unstructured":"C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231\u2013261, July 1996.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"T. Johnsson. Efficient compilation of lazy evaluation. In Proceedings of the ACM Conference on Compiler Construction, pages 122\u201332, 1984.","DOI":"10.1145\/502874.502880"},{"key":"23_CR25","unstructured":"R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In ICCAD, 1995."},{"key":"23_CR26","unstructured":"J. Joyce. Multi-Level Verification of Microprocessor Based Systems. PhD thesis, Cambridge Comp. Lab, 1989. Technical Report 195."},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"J. Joyce, N. Day, and M. Donat. S: A machine readable specification notation based on higher order logic. In International Workshop on the HOL Theorem Proving System and its Applications, pages 285\u2013299, 1994.","DOI":"10.1007\/3-540-58450-1_49"},{"issue":"9","key":"23_CR28","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. G. Leveson","year":"1994","unstructured":"N. G. Leveson et al. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9):684\u2013707, September 1994.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T14:21:02Z","timestamp":1676643662000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-48256-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 September 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}