{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:29Z","timestamp":1759147109347,"version":"3.43.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2000,3,1]],"date-time":"2000-03-01T00:00:00Z","timestamp":951868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,3,1]],"date-time":"2000-03-01T00:00:00Z","timestamp":951868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,3]]},"DOI":"10.1023\/a:1008791128550","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"127-158","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning About Analog-Level Implementations of Digital Systems"],"prefix":"10.1007","volume":"16","author":[{"given":"Keith","family":"Hanna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"254637_CR1","doi-asserted-by":"crossref","unstructured":"D. A. Basin, \u201cVerification of combinational logic in Nuprl,\u201d in M. Leeser and G. Brown (Eds.), Hardware Specification, Verification and Synthesis: Mathematical Aspects, Springer Verlag, 1990. LNCS, Vol. 408, pp. 333\u2013357.","DOI":"10.1007\/0-387-97226-9_36"},{"key":"254637_CR2","unstructured":"R. Boute, \u201cFunmath illustrated; a declarative formalism and application examples,\u201d Technical Report, Department of Informatics, Katholieke Universiteit Nijmegen, July 1993."},{"key":"254637_CR3","doi-asserted-by":"crossref","unstructured":"G. M. Brown and M. E. Leeser, \u201cFrom programs to transistors: Verifying hardware synthesis tools,\u201d in M. Leeser and G. Brown (Eds.), Hardware Specification, Verification and Synthesis: Mathematical Aspects, Springer Verlag, 1990. LNCS, Vol. 408, pp. 129\u201315.","DOI":"10.1007\/0-387-97226-9_27"},{"key":"254637_CR4","unstructured":"M. Gordon, \u201cWhyhigher-order logic is a good formalism for specifying and verifying hardware,\u201d in G.J. Milner and P.A. Subrahmanyam (Eds.), Formal Aspects of VLSI Design: Proc. of the 1985 Edinburgh Workshop on VLSI, North-Holland, pp. 153\u2013177, 1986."},{"key":"254637_CR5","unstructured":"M. Gordon, P. Loewenstein, and M. Shahaf, \u201cFormal verification of a cell library,\u201d in L.J.M. Claesen (Ed.), VLSI Design Methods II, Elsevier Science Publishers B.V., 1990, pp. 409\u2013417."},{"key":"254637_CR6","doi-asserted-by":"crossref","unstructured":"F.K. Hanna and N. Daeche, \u201cSpecification and verification of digital systems using higher-order logic,\u201d Proc. IEE, Part E, pp. 242\u2013254, 1986.","DOI":"10.1049\/ip-e.1986.0031"},{"key":"254637_CR7","unstructured":"F.K. Hanna and N. Daeche, \u201cSpecification and verification using higher-order logic: A case study,\u201d inMilne and Subrahmanyam (Eds.), Formal Aspects of VLSI Design, North Holland, 1986, pp. 179\u2013213."},{"key":"254637_CR8","doi-asserted-by":"crossref","unstructured":"K. Hanna, \u201cReasoning about real digital circuits,\u201d in Proc Higher Order Logic Theorem Proving and its Applications, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_46"},{"key":"254637_CR9","doi-asserted-by":"crossref","unstructured":"K. Hanna, \u201cAutomatic verification of mixed-level logic circuits,\u201d in G. Gopalakrishnan and P. Windley (Eds.), Formal Methods in Computer-Aided Design; FMCAD 98, Springer-Verlag, 1998, pp. 133\u2013148.","DOI":"10.1007\/3-540-49519-3_10"},{"key":"254637_CR10","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(91)90309-P","volume":"90","author":"C.A.R. Hoare","year":"1991","unstructured":"C.A.R. Hoare, \u201cA theory for the derivation of combinational C-mos circuit designs,\u201d Theoretical Computer Science, Vol. 90, pp. 235\u2013251, 1991.","journal-title":"Theoretical Computer Science"},{"key":"254637_CR11","unstructured":"D.A. Hodges and H.G. Jackson, Analysis and Design of Digital Integrated Circuits, McGraw-Hill, 1983."},{"key":"254637_CR12","unstructured":"IEEE-DASC, \u201cIEEE standard VHDL-AMS language reference manual,\u201d Technical Report Draft IEEE Std 1076.1-1997, IEEE Computer Society, 1997."},{"key":"254637_CR13","doi-asserted-by":"crossref","unstructured":"T. Melham, Higher Order Logic and Hardware Verification, Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511569845"},{"issue":"4","key":"254637_CR14","first-page":"529","volume":"24","author":"R.E. Shostak","year":"1977","unstructured":"R.E. Shostak, \u201cOn the SUP-INF method for proving Presburger formulas,\u201d ACM, Vol. 24, No. 4, pp. 529\u2013543, 1977.","journal-title":"ACM"},{"key":"254637_CR15","unstructured":"R.E. Shostak, \u201cFormal verification of circuit designs,\u201d in T. Uehara and M. Barbacci (Eds.), Computer Hardware Description Languages and their Applications, North-Holland, 1983, pp. 13\u201330."},{"key":"254637_CR16","doi-asserted-by":"crossref","unstructured":"D. Weise, \u201cConstraints, abstraction and verification,\u201d in M. Leeser and G. Brown (Eds.), Hardware Specification, Verification and Synthesis: Mathematical Aspects, Springer Verlag, 1989. LNCS, Vol. 408, pp. 25\u201339.","DOI":"10.1007\/0-387-97226-9_22"},{"key":"254637_CR17","doi-asserted-by":"crossref","unstructured":"G. Winskel, \u201cModels and logic of MOS circuits,\u201d in M. Broy (Ed.), Logic of Programming and Calculi of Discrete Design, Springer-Verlag, 1987. NATO ASI series, Vol. F36, pp. 367\u2013413.","DOI":"10.1007\/978-3-642-87374-4_14"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008791128550.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008791128550\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008791128550.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:19:33Z","timestamp":1754367573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008791128550"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,3]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,3]]}},"alternative-id":["254637"],"URL":"https:\/\/doi.org\/10.1023\/a:1008791128550","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,3]]}}}