{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:37Z","timestamp":1725484297674},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_15","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"214-229","source":"Crossref","is-referenced-by-count":1,"title":["PuzzleTool: An Example of Programming Computation and Deduction"],"prefix":"10.1007","author":[{"given":"Michael J. C.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs\u201999)","author":"M. D. Aagaard","year":"1999","unstructured":"Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Theorem Proving in Higher Order Logics (TPHOLs\u201999), number 1690 in Lecture Notes in Computer Science, pages 323\u2013340. Springer-Verlag, 1999."},{"key":"15_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"B. Barras","year":"2000","unstructured":"Bruno Barras. Programming and computing in HOL. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 17\u201337. Springer-Verlag, 2000."},{"key":"15_CR3","unstructured":"See web page \n                    http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\n                    \n                  ."},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for Constructing Systems (TACAS 2000)","author":"L. A. Dennis","year":"2000","unstructured":"L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The prosper toolkit. In S. Graf and M. Schwartbach, editors, Tools and Algorithms for Constructing Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 78\u201392. Springer-Verlag, 2000."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-44659-1_12","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"M. J.C. Gordon","year":"2000","unstructured":"Michael J.C. Gordon. Reachability programming in HOL using BDDs. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 180\u2013197. Springer-Verlag, 2000."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Mike Gordon. Reachability programming in HOL98 using BDDs. In The 13th International Conference on Theorem Proving and Higher Order Logics. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_12"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1093\/comjnl\/38.2.162","volume":"38","author":"J. Harrison","year":"1995","unstructured":"John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162\u2013170, 1995.","journal-title":"The Computer Journal"},{"key":"15_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-57826-9_135","volume-title":"Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG\u201993, Vancouver, B.C., August 11\u201313 1993","author":"J. Joyce","year":"1994","unstructured":"J. Joyce and C. Seger. The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG\u201993, Vancouver, B.C., August 11\u201313 1993, volume 780 of Lecture Notes in Computer Science, pages 185\u2013198. Spinger-Verlag, 1994."},{"key":"15_CR9","unstructured":"Moscow ML interface to BuDDy by Ken Friis Larsen and Jakob Lichtenberg documented at \n                    http:\/\/www.it-c.dk\/research\/muddy\/\n                    \n                  ."},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer-Aided Verification, CAV\u2019 97","author":"K.L. McMillan","year":"1997","unstructured":"K.L. McMillan. A compositional rule for hardware design refinement. In Orna Grumberg, editor, Computer-Aided Verification, CAV\u2019 97, Lecture Notes in Computer Science, pages 24\u201335, Haifa, Israel, June 1997. Springer-Verlag."},{"key":"15_CR11","unstructured":"John O\u2019Leary, Xudong Zhao, Robert Gerth, and Carl-Johan H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, First Quarter 1999. Online at \n                    http:\/\/developer.intel.com\/technology\/itj\/\n                    \n                  ."},{"key":"15_CR12","unstructured":"See web page \n                    http:\/\/www.csl.sri.com\/pvs.html\n                    \n                  ."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, CAV\u201995","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV\u201995, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995. Springer-Verlag."},{"key":"15_CR14","unstructured":"Carl-Johan H. Seger. Voss-a formal hardware verification system: User\u2019s guide. Technical Report UBC TR 93-45, The University of British Columbia, December 1993."},{"key":"15_CR15","unstructured":"Fabio Somenzi\u2019s CUDD: CU Decision Diagram Package documented at \n                    http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/\n                    \n                  ."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T15:02:28Z","timestamp":1550329348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}