{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T17:20:42Z","timestamp":1761931242154,"version":"build-2065373602"},"reference-count":20,"publisher":"Elsevier BV","issue":"1-5","license":[{"start":{"date-parts":[[1990,8,1]],"date-time":"1990-08-01T00:00:00Z","timestamp":649468800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Microprocessing and Microprogramming"],"published-print":{"date-parts":[[1990,8]]},"DOI":"10.1016\/0165-6074(90)90277-g","type":"journal-article","created":{"date-parts":[[2003,9,3]],"date-time":"2003-09-03T17:14:48Z","timestamp":1062609288000},"page":"421-428","source":"Crossref","is-referenced-by-count":3,"title":["The OTTER environment for resolution-based proof of hardware correctness"],"prefix":"10.1016","volume":"30","author":[{"given":"Paolo","family":"Camurati","sequence":"first","affiliation":[]},{"given":"Tiziana","family":"Margaria","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Prinetto","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0165-6074(90)90277-G_BIB1","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/0004-3702(84)90044-4","article-title":"VERIFY: a program for proving correctness of digital hardware designs","volume":"Vol. 24","author":"Barrow","year":"1984","journal-title":"Artificial intelligence"},{"year":"1988","author":"Boyer","key":"10.1016\/0165-6074(90)90277-G_BIB2"},{"key":"10.1016\/0165-6074(90)90277-G_BIB3","series-title":"IFIP TC-10 Conference: \u201cDesign Methodologies for VLSI and Computer Architecture\u201d","first-page":"147","article-title":"Simulation as an aid to verification using the HOL theorem prover","author":"Camilleri","year":"1988"},{"issue":"n. 7","key":"10.1016\/0165-6074(90)90277-G_BIB4","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.65","article-title":"Formal verification of hardware correctness: introduction and survey of current research","volume":"Vol. 21","author":"Camurati","year":"1988","journal-title":"IEEE COMPUTER"},{"key":"10.1016\/0165-6074(90)90277-G_BIB5","first-page":"50","article-title":"Formal verification: is it practical for real-world design?","author":"Camurati","year":"1989","journal-title":"IEEE Design & Test of Computers"},{"year":"1973","series-title":"Symbolic logic and mechanical theorem proving","author":"Chang","key":"10.1016\/0165-6074(90)90277-G_BIB6"},{"year":"1981","series-title":"Programming in Prolog","author":"Clocksin","key":"10.1016\/0165-6074(90)90277-G_BIB7"},{"key":"10.1016\/0165-6074(90)90277-G_BIB8","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0743-1066(87)90022-7","article-title":"Logic programming and digital circuit analysis","volume":"4","author":"Clocksin","year":"1987","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/0165-6074(90)90277-G_BIB9","series-title":"IMEC-IFIP Workshop on \u201cApplied Formal Methods For Correct VLSI Design\u201d","article-title":"Special session on benchmarks","author":"Claesen","year":"1989"},{"key":"10.1016\/0165-6074(90)90277-G_BIB10","series-title":"CHDL '85: IFIP 7th Int. Symposium on Computer Hardware Description Languages and their Applications","first-page":"167","article-title":"The application of CHDL's to the abstract specification of hardware","author":"Eveking","year":"1985"},{"article-title":"LCF-LSM: a system for specifying and verifying hardware","year":"1984","author":"Gordon","key":"10.1016\/0165-6074(90)90277-G_BIB11"},{"article-title":"HOL: a machine oriented formulation of Higher Order Logic","year":"1985","author":"Gordon","key":"10.1016\/0165-6074(90)90277-G_BIB12"},{"article-title":"Introducing OBJ3","year":"1988","author":"Goguen","key":"10.1016\/0165-6074(90)90277-G_BIB13"},{"key":"10.1016\/0165-6074(90)90277-G_BIB14","series-title":"IFIP WG 10.2 Workshop \u201cFrom HDL descriptions to guaranteed correct circuit designs\u201d","first-page":"85","article-title":"FM8501: a verified microprocessor","author":"Hunt","year":"1986"},{"article-title":"The automated reasoning system ITP","year":"1984","author":"Lusk","key":"10.1016\/0165-6074(90)90277-G_BIB15"},{"year":"1986","series-title":"Logic Design Principles with Emphasis on Testable Semicustom Circuits","author":"McCluskey","key":"10.1016\/0165-6074(90)90277-G_BIB16"},{"key":"10.1016\/0165-6074(90)90277-G_BIB17","unstructured":"W.W. McCune: \u201cOTTER 1.0 User's Guide,\u201d Rep. ANL-88-44 Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL (USA)"},{"key":"10.1016\/0165-6074(90)90277-G_BIB18","series-title":"CHDL '83: IFIP 6th Int. Symposium on Computer Hardware Description Languages and their Applications","first-page":"79","article-title":"A temporal Logic for multi-level reasoning about hardware","author":"Moszkowski","year":"1983"},{"key":"10.1016\/0165-6074(90)90277-G_BIB19","first-page":"129","article-title":"The formal proof of the \u201cMin-max\u201d sequential benchmark described in CASCADE using the Boyer-Moore theorem prover","volume":"Vol. 1","author":"Pierre","year":"1989"},{"article-title":"Reference manual for the environmental theorem prover: an incarnation of AURA","year":"1988","author":"Smith","key":"10.1016\/0165-6074(90)90277-G_BIB20"}],"container-title":["Microprocessing and Microprogramming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016560749090277G?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016560749090277G?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T10:20:10Z","timestamp":1551090010000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016560749090277G"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,8]]},"references-count":20,"journal-issue":{"issue":"1-5","published-print":{"date-parts":[[1990,8]]}},"alternative-id":["016560749090277G"],"URL":"https:\/\/doi.org\/10.1016\/0165-6074(90)90277-g","relation":{},"ISSN":["0165-6074"],"issn-type":[{"type":"print","value":"0165-6074"}],"subject":[],"published":{"date-parts":[[1990,8]]}}}