{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T08:37:19Z","timestamp":1775291839327,"version":"3.50.1"},"reference-count":49,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2003.1210044","type":"proceedings-article","created":{"date-parts":[[2003,12,22]],"date-time":"2003-12-22T12:34:10Z","timestamp":1072096450000},"page":"45-54","source":"Crossref","is-referenced-by-count":15,"title":["Formal verification at Intel"],"prefix":"10.1109","author":[{"given":"J.","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"35","author":"oostdijk","year":"2001","journal-title":"Generation and Presentation of Formal Mathematical Documents"},{"key":"36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3540-6","author":"peled","year":"2001","journal-title":"Software Reliability Methods"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1147\/rd.341.0111"},{"key":"34","article-title":"Formally verifying IEEE compliance of floating-point hardware","author":"o'leary","year":"1999","journal-title":"Intel Technology Journal"},{"key":"39","first-page":"195","article-title":"Specification and verification of concurrent programs in CESAR","volume":"137","author":"queille","year":"1982","journal-title":"Lecture Notes in Computer Science"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1137\/0204018"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59293-8_189"},{"key":"43","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383966"},{"key":"42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22646-9"},{"key":"41","author":"rudnicki","year":"1992","journal-title":"An Overview of the MIZAR Project"},{"key":"40","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","article-title":"An integration of model-checking with automated proof-checking","volume":"939","author":"rajan","year":"1995","journal-title":"Lecture Notes in Computer Science"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"23","first-page":"159","article-title":"Complex quantifier elimination in HOL","volume":"edi inf rr 46","author":"harrison","year":"2001","journal-title":"TPHOLs 2001 Supplemental Proceedings"},{"key":"24","doi-asserted-by":"crossref","DOI":"10.1109\/ARITH.2003.1207673","article-title":"Isolating critical cases for reciprocals using integer factorization","author":"harrison","year":"2003","journal-title":"Proc 10th IEEE Symp Computer Arithmetic"},{"key":"25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","article-title":"A sceptic's approach to combining HOL and Maple","volume":"21","author":"harrison","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"26","year":"1985","journal-title":"A Standard for Binary Floating-Point Arithmetic"},{"key":"27","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-44659-1_21","article-title":"Divider circuit verification with model checking and theorem proving","volume":"1869","author":"kaivola","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"28","author":"kaufmann","year":"2000","journal-title":"Computer-Aided Reasoning ACL2 Case Studies"},{"key":"29","author":"kaufmann","year":"2000","journal-title":"Computer-Aided Reasoning An Approach"},{"key":"3","author":"baker","year":"1985","journal-title":"A Concise Introduction to the Theory of Numbers"},{"key":"2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46419-0_28","article-title":"Symbolic reachability analysis based on SAT-solvers","volume":"1785","author":"abdulla","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","article-title":"Lifted-FL: A pragmatic implementation of combined model checking and theorem proving","volume":"1690","author":"aagaard","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"7","first-page":"419","article-title":"Symbolic verification of MOS circuits","author":"bryant","year":"1985","journal-title":"Proceedings of the 1985 Chapel Hill Conference on VLSI"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03809-3"},{"key":"6","article-title":"Efficiency in a fully-expansive theorem prover","volume":"337","author":"boulton","year":"1993","journal-title":"Technical Report"},{"key":"5","first-page":"133","article-title":"Boyer-Moore automation for the HOL system","volume":"a 20","author":"boulton","year":"1992","journal-title":"IFIP Transactions A Computer Science and Technology"},{"key":"32","author":"markstein","year":"2000","journal-title":"IA-64 and Elementary Functions Speed and Precision"},{"key":"4","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1109\/HOL.1991.596284"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1979.1600119"},{"key":"8","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","article-title":"Automatic verification of pipelined microprocessor control","volume":"818","author":"burch","year":"1994","journal-title":"Lecture Notes in Computer Science"},{"key":"19","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","article-title":"HOL light: A tutorial introduction","volume":"1166","author":"harrison","year":"1996","journal-title":"Lecture Notes in Computer Science"},{"key":"17","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","article-title":"Edinburgh LCF: A mechanised logic of computation","volume":"78","author":"gordon","year":"1979","journal-title":"Lecture Notes in Computer Science"},{"key":"18","author":"graham","year":"1994","journal-title":"Concrete Mathematics A Foundation for Computer Science"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"key":"16","author":"gordon","year":"1993","journal-title":"Introduction to HOL A Theorem Proving Environment for Higher Order Logic"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"14","author":"dijkstra","year":"1976","journal-title":"A Discipline of Programming"},{"key":"11","article-title":"Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms","author":"cornea-hasegan","year":"1998","journal-title":"Intel Technology Journal"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139173018"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097791"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105406"},{"key":"49","article-title":"A theory for generalized symbolic trajectory evaluation","author":"yang","year":"2000","journal-title":"Proceedings of the 2000 Symposium on Symbolic Trajectory Evaluation"},{"key":"48","author":"weis","year":"1993","journal-title":"Le Langage Caml InterEditions"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"44","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","article-title":"A tutorial on Sta?lmarck's proof procedure for prepositional logic","volume":"1522","author":"sheeran","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"47","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","article-title":"Superscalar processor verification using efficient reduction of hte logic of equality with uninterpreted functions to prepositional logic","volume":"1703","author":"velev","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"46","first-page":"136","article-title":"The Mizar-QC\/6000 logic information language","volume":"6","author":"trybulec","year":"1978","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"10","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","article-title":"Design and synthesis of synchronization skeletons using branching-time temporal logic","volume":"131","author":"clarke","year":"1981","journal-title":"Lecture Notes in Computer Science"}],"event":{"name":"18th Annual IEEE Symposium on Logic in Computer Science","location":"Ottawa, Ont., Canada","acronym":"LICS-03"},"container-title":["18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8592\/27231\/01210044.pdf?arnumber=1210044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,15]],"date-time":"2017-06-15T22:58:18Z","timestamp":1497567498000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210044\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":49,"URL":"https:\/\/doi.org\/10.1109\/lics.2003.1210044","relation":{},"subject":[]}}