{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:59Z","timestamp":1725488639071},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_22","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"323-340","source":"Crossref","is-referenced-by-count":22,"title":["Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[]},{"given":"Robert B.","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Carl-Johan H.","family":"Seger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In DAC, pages 538\u2013541. ACM\/IEEE, July 1998.","DOI":"10.1145\/277044.277189"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Formal verification using parametric representations of Boolean constraints. In DAC, July 1999.","DOI":"10.1145\/309847.309968"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard and C.-J. H. Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier. In ICCAD, pages 7\u201310. IEEE Comp. Soc. Press, Washington D.C. Nov. 1995.","DOI":"10.1109\/ICCAD.1995.479878"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"L. Augustson. A compiler for Lazy-ML. In ACM Symposium on Lisp and Functional Programming, pages 218\u2013227, 1984.","DOI":"10.1145\/800055.802038"},{"key":"22_CR5","unstructured":"D. E. Beatty, R. E. Bryant, and C.-J. H. Seger. Synchronous circuit verification \u2014 an illustration. In Advanced Research in VLSI, Proceedings of the Sixth MIT Conference, pages 98\u2013112. MIT Press, 1990."},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0055129","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Bhargavan","year":"1998","unstructured":"K. Bhargavan, C.A. Gunter, E. L. Gunter, M. Jackson, D. Obradovic, and P. Zave. The village telephone system: A case study in formal software engineering. In M. Newey and J. Grundy, editors, Theorem Proving in Higher Order Logics, pages 49\u201366. Springer Verlag; New York, Sept. 1998."},{"issue":"8","key":"22_CR7","first-page":"677","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on CAD, C-35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Trans. on CAD"},{"issue":"5","key":"22_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. on Prog. Lang. and Systems, 16(5):1512\u20131542, Sept. 1994.","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"22_CR9","first-page":"227","volume-title":"LICS","author":"T. Coquand","year":"1986","unstructured":"T. Coquand. An analysis of Girard\u2019s paradox. In LICS, pages 227\u2013236. IEEE Comp. Soc. Press, Washington D.C. June 1986."},{"key":"22_CR10","unstructured":"P. Curzon, S. Tahar, and O. A. Mohamed. Verification of the MDG components library in HOL. Technical Report 98-08, Australian Nat\u2019l Univ., Comp. Sci., 1998. pages 31\u201346 In Supplementary Proceedings of TPHOLS-98."},{"key":"22_CR11","unstructured":"J. M. Feldman and C. T. Retter. Computer Architecture. McGraw-Hill, 1994."},{"key":"22_CR12","unstructured":"A. Field and P. Harrison. Functional Programming. Addison Wesley, 1988."},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","key":"22_CR13","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York, 1993."},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BFb0055134","volume-title":"Theorem Proving in Higher Order Logics","author":"E. L. Gunter","year":"1998","unstructured":"E. L. Gunter. Adding external decision procedures to HOL90 securely. In M. Newey and J. Grundy, editors, Theorem Proving in Higher Order Logics, pages 143\u2013152. Springer Verlag; New York, Sept. 1998."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"S. Hazelhurst and C.-J. H. Seger. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Trans. on CAD, Apr. 1995.","DOI":"10.1109\/43.372367"},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3\u201378. Springer Verlag; New York, 1997."},{"key":"22_CR17","unstructured":"IEEE. IEEE Standard for binary floating-point arithmetic. ANSI\/IEEE Std 754-1985, 1985."},{"issue":"1","key":"22_CR18","first-page":"41","volume":"9","author":"N. C. Ip","year":"1996","unstructured":"N. C. Ip and D. L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1\/2):41\u201375, Aug. 1996.","journal-title":"Formal Methods in System Design"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"J. Joyce and C.-J. Seger. Linking BDD based symbolic evaluation to interactive theorem proving. In DAC, June 1993.","DOI":"10.1145\/157485.164981"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"M. Kaufmann and J. Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. on Soft. Eng., 1997.","DOI":"10.1109\/32.588534"},{"key":"22_CR21","first-page":"1","volume-title":"Formal Methods in CAD","author":"K. McMillan","year":"1998","unstructured":"K. McMillan. Minimalist proof assistants: Interactions of technology and methodology in formal system level verification. In G. C. Gopalakrishnan and P. J. Windley, editors, Formal Methods in CAD, page 1. Springer Verlag; New York, Nov. 1998."},{"key":"22_CR22","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Tech. Jour., First Quarter 1999. Online at http:\/\/developer.intel.com\/technology\/itj\/ ."},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"L. Paulson. ML for the Working Programmer,. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"key":"22_CR24","volume-title":"CAV","author":"S. Rajan","year":"1996","unstructured":"S. Rajan, N. Shankar, and M. Srivas. An integration of model checking automated proof checking. In CAV. Springer Verlag; New York, 1996."},{"key":"22_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"CAV","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. A. J. Hunt. Processor verification with precise exeptions and speculative execution. In A. Hu and M. Vardi, editors, CAV, number 1427 in LNCS, pages 135\u2013146. Springer Verlag; New York, June 1998."},{"issue":"2","key":"22_CR26","doi-asserted-by":"publisher","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(2):147\u2013189, Mar. 1995.","journal-title":"Formal Methods in System Design"},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0028400","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1997","unstructured":"K. Slind. Derivation and use of induction schemes in higher-order logic. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics, pages 275\u2013291. Springer Verlag; New York, Aug. 1997."}],"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-48256-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T14:58:47Z","timestamp":1556722727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}