{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:32:23Z","timestamp":1757626343816,"version":"3.44.0"},"reference-count":41,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1989,9,1]],"date-time":"1989-09-01T00:00:00Z","timestamp":620611200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1989,9,1]],"date-time":"1989-09-01T00:00:00Z","timestamp":620611200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Integration"],"published-print":{"date-parts":[[1989,9]]},"DOI":"10.1016\/0167-9260(89)90004-7","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T14:37:33Z","timestamp":1047652653000},"page":"247-266","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal specification and verification of microprocessor systems"],"prefix":"10.1016","volume":"7","author":[{"given":"Jeffrey J.","family":"Joyce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/0167-9260(89)90004-7_BIB1","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/TC.1981.6312154","article-title":"Instruction set processor specification (ISPS): the notation and its application","volume":"C-30","author":"Barbacci","year":"1981","journal-title":"IEEE Trans. on Comput."},{"key":"10.1016\/0167-9260(89)90004-7_BIB2","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":"24","author":"Barrow","year":"1984","journal-title":"Artif. Intell."},{"key":"10.1016\/0167-9260(89)90004-7_BIB3","series-title":"Tech. Monograph PRG-60","article-title":"The formal specification of a microprocessor instruction set","author":"Bowen","year":"1987"},{"key":"10.1016\/0167-9260(89)90004-7_BIB4","series-title":"Ph.D. Thesis, Dept. of Electrical Engineering and Computer Science, Tech. Report MIT\/LCS\/TR-259","article-title":"A switch-level simulation model for integrated logic circuits","author":"Bryant","year":"1981"},{"article-title":"Executing behavioural definitions in higher order logic","year":"1988","author":"Camilleri","key":"10.1016\/0167-9260(89)90004-7_BIB5"},{"key":"10.1016\/0167-9260(89)90004-7_BIB6","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":"J. Logic Program."},{"key":"10.1016\/0167-9260(89)90004-7_BIB7","series-title":"VLSI Specification, Verification and Synthesis","first-page":"27","article-title":"A proof of correctness of the VIPER microprocessor: the first level","author":"Cohn","year":"1988"},{"key":"10.1016\/0167-9260(89)90004-7_BIB8","series-title":"VLSI Specification, Verification and Synthesis","first-page":"1","article-title":"Implementing safety-critical systems: the VIPER microprocessor","author":"Cullyer","year":"1988"},{"key":"10.1016\/0167-9260(89)90004-7_BIB9_1","series-title":"VLSI Specification, Verification and Synthesis","first-page":"293","article-title":"Formal validation of an integrated circuit design style","author":"Dhingra","year":"1988"},{"year":"1987","series-title":"Report 115","key":"10.1016\/0167-9260(89)90004-7_BIB9_2"},{"year":"1986","series-title":"Ferranti Semiconductors, VIP 1, Produce release announcement, VIP 19\/86","key":"10.1016\/0167-9260(89)90004-7_BIB10"},{"year":"1979","series-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"Gordon","key":"10.1016\/0167-9260(89)90004-7_BIB11"},{"key":"10.1016\/0167-9260(89)90004-7_BIB12","series-title":"Tech. Report No. 42","article-title":"Proving a computer correct using the LCF-LSM hardware verification system","author":"Gordon","year":"1983"},{"key":"10.1016\/0167-9260(89)90004-7_BIB13","series-title":"Formal Aspects of VLSI Design","first-page":"153","article-title":"Why higher-order logic is a good formalism for specifying and verifying hardware","author":"Gordon","year":"1986"},{"key":"10.1016\/0167-9260(89)90004-7_BIB14_1","series-title":"VLSI Specification, Verification and Synthesis","first-page":"73","article-title":"A proof generating system for higher-order logic","author":"Gordon","year":"1988"},{"year":"1987","series-title":"Report No. 103","key":"10.1016\/0167-9260(89)90004-7_BIB14_2"},{"key":"10.1016\/0167-9260(89)90004-7_BIB15","series-title":"Current Trends in Hardware Verification and Automated Theorem Proving","first-page":"387","article-title":"Mechanizing programming logics in higher order logic","author":"Gordon","year":"1989"},{"year":"1980","series-title":"Functional Programming","author":"Henderson","key":"10.1016\/0167-9260(89)90004-7_BIB16"},{"article-title":"Application of formal methods to digital system design","year":"1986","author":"Herbert","key":"10.1016\/0167-9260(89)90004-7_BIB17"},{"key":"10.1016\/0167-9260(89)90004-7_BIB18","first-page":"73","article-title":"High-level microprogramming support embedded in silicon","volume":"135","author":"Hobson","year":"1981"},{"article-title":"FM8501: a verified microprocessor","year":"1986","author":"Hunt","key":"10.1016\/0167-9260(89)90004-7_BIB19"},{"key":"10.1016\/0167-9260(89)90004-7_BIB20","series-title":"Report No. 100","article-title":"Proving a computer correct in higher order logic","author":"Joyce","year":"1986"},{"key":"10.1016\/0167-9260(89)90004-7_BIB21","series-title":"VLSI Specification, Verification and Synthesis","first-page":"129","article-title":"Formal verification and implementation of a microprocessor","author":"Joyce","year":"1988"},{"key":"10.1016\/0167-9260(89)90004-7_BIB22","series-title":"IFIP WG 10.2 International Workshop on Design for Behavioural Verification","article-title":"Generic structures in the formal specification and verification of digital circuits","author":"Joyce","year":"1988"},{"article-title":"Formal specification and verification of asynchronous processes in higher-order logic","series-title":"Workshop on Specification and Verification of Concurrent Processes","author":"Joyce","key":"10.1016\/0167-9260(89)90004-7_BIB23_1"},{"year":"1988","series-title":"Report No. 136","key":"10.1016\/0167-9260(89)90004-7_BIB23_2"},{"article-title":"Reasoning about the function and timing of integrated circuits with prolog and temporal logic","year":"1987","author":"Leeser","key":"10.1016\/0167-9260(89)90004-7_BIB24"},{"year":"1986","series-title":"Marconi Electronic Devices, VIPER 32 bit microprocessor","key":"10.1016\/0167-9260(89)90004-7_BIB25"},{"key":"10.1016\/0167-9260(89)90004-7_BIB26","series-title":"Internal Report","article-title":"Formal verification of the IMS T800 microprocessor","author":"May","year":"1987"},{"key":"10.1016\/0167-9260(89)90004-7_BIB27","series-title":"VLSI Specification, Verification and Synthesis","first-page":"267","article-title":"Abstraction mechanisms for hardware verification","author":"Melham","year":"1988"},{"key":"10.1016\/0167-9260(89)90004-7_BIB28","first-page":"127","article-title":"Behavioural description and VLSI verification","volume":"133","author":"Milne","year":"1986"},{"article-title":"Reasoning about digital circuits","year":"1983","author":"Moszkowski","key":"10.1016\/0167-9260(89)90004-7_BIB29"},{"year":"1986","series-title":"Executing Temporal Logic Programs","author":"Moszkowski","key":"10.1016\/0167-9260(89)90004-7_BIB30"},{"year":"1975","series-title":"SPICE2: a computer program to simulate semiconductor circuits","author":"Nagel","key":"10.1016\/0167-9260(89)90004-7_BIB31"},{"year":"1987","series-title":"Logic and Computation","author":"Paulson","key":"10.1016\/0167-9260(89)90004-7_BIB32"},{"key":"10.1016\/0167-9260(89)90004-7_BIB33","series-title":"Tech. Report No. 84","article-title":"BSPL: a language for describing the behaviour of synchronous hardware","author":"Richards","year":"1986"},{"key":"10.1016\/0167-9260(89)90004-7_BIB34","first-page":"295","article-title":"Design and verification of regular synchronous circuits","volume":"133","author":"Sheeran","year":"1986"},{"issue":"7","key":"10.1016\/0167-9260(89)90004-7_BIB35","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/C-M.1981.220524","article-title":"Scheme-79: lisp on a chip","volume":"14","author":"Sussman","year":"1981","journal-title":"IEEE Comput."},{"issue":"2","key":"10.1016\/0167-9260(89)90004-7_BIB36","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/MSPEC.1987.6448028","article-title":"Designing micro-based systems for fail-safe travel","volume":"24","author":"Turner","year":"1987","journal-title":"IEEE Spectrum"},{"article-title":"Formal multilevel hierarchical verification of synchronous MOS VLSI circuits","year":"1986","author":"Weise","key":"10.1016\/0167-9260(89)90004-7_BIB37"},{"key":"10.1016\/0167-9260(89)90004-7_BIB38","series-title":"VLSI Specification, Verification and Synthesis","first-page":"323","article-title":"Models and logic of MOS circuits","author":"Winskel","year":"1988"}],"container-title":["Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167926089900047?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167926089900047?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T21:36:56Z","timestamp":1757453816000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167926089900047"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,9]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,9]]}},"alternative-id":["0167926089900047"],"URL":"https:\/\/doi.org\/10.1016\/0167-9260(89)90004-7","relation":{},"ISSN":["0167-9260"],"issn-type":[{"type":"print","value":"0167-9260"}],"subject":[],"published":{"date-parts":[[1989,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Formal specification and verification of microprocessor systems","name":"articletitle","label":"Article Title"},{"value":"Integration","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/0167-9260(89)90004-7","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1989 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}