{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T19:08:44Z","timestamp":1761937724893,"version":"build-2065373602"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1995,6,1]],"date-time":"1995-06-01T00:00:00Z","timestamp":801964800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1995,6]]},"DOI":"10.1007\/bf01384501","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T04:22:41Z","timestamp":1112415761000},"page":"295-320","source":"Crossref","is-referenced-by-count":7,"title":["Localized verification of modular designs"],"prefix":"10.1007","volume":"6","author":[{"given":"J\ufffdrgen","family":"Staunstrup","sequence":"first","affiliation":[]},{"given":"Niels","family":"Mellergaard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"R.E. Bryant, ?Can a Simulator Verify a Circuit??Formal Aspects of VLSI Design, North-Holland, 1985, pp. 125?136."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"K. Mani Chandy and J. Misra,Parallel Program Design: A Foundation, Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"R.W. Floyd, ?Assigning meanings to programs,? in J.T. Schwartz, editor,Proceedings of the Symposium in Applied Mathematics, American Mathematical Society, 1967, Vol. 19, pp. 19?32.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"CR4","unstructured":"Michael P. Fourman and Robert L. Harris, ?Lambda?logic and mathematics behind design automation,? inProceedings of the 26th ACM\/IEEE Design Automation Conference, ACM, 1989."},{"key":"CR5","unstructured":"Stephen J. Garland and John V. Guttag, ?A guide to LP, the Larch Prover,? Technical Report 82, Digital SRC, 1991."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Stephen J. Garland, John V. Guttag, and J\u00f8rgen Staunstrup, ?Verification of VLSI circuits using LP,? inThe Fusion of Hardware Design and Verification, IFIP WG. 10.2, North Holland, 1988, pp. 329?346.","DOI":"10.7146\/dpb.v17i258.7842"},{"key":"CR7","unstructured":"Mike Gordon, ?Why higher-order logic is a good formalism for specifying and verifying hardware,? inFormal Aspects of VLSI Design, North-Holland, 1985, pp. 153?177."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Mike Gordon, ?HOL A Proof Generating System for Higher-Order Logic,?VLSI Specification, Verification and Synthesis, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"issue":"2\/3","key":"CR9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"Aarti Gupta","year":"1992","unstructured":"Aarti Gupta, ?Formal hardware verification methods: A survey,?Formal Methods in Systems Design, 1(2\/3):151?238, October 1992.","journal-title":"Formal Methods in Systems Design"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"John V. Guttag, James J. Horning, S.J. Garland, K.D. Jones, A. Modet, and J.M. Wing,Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"CR11","unstructured":"Warren A. Hunt, ?FM8501: A verified microprocessor,? inFrom HDL Descriptions to Guaranteed Correct Circuit Designs, North-Holland, 1986, pp. 85?114."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce, ?Generic specification of digital hardware,? inDesigning Correct Circuits, Oxford 1990, Springer-Verlag, 1991, pp. 68?91.","DOI":"10.1007\/978-1-4471-3544-9_4"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"J.C. Madre and J.P. Billon, ?Proving circuit correctness using formal comparison between expected and extracted behavior,?Proceedings of the 25th ACM\/IEEE Design Automation Conference, ACM, 1988, pp. 205?210.","DOI":"10.1109\/DAC.1988.14759"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Niels Maretti, ?Mechanized verification of refinement,? inProceedings from TPCD'94, Springer Lecture Notes, Vol. 901, pp. 185?202.","DOI":"10.1007\/3-540-59047-1_49"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan,Symbolic Model Checking, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"CR16","unstructured":"Niels Mellergaard, ?Mechanized Design Verification,? PhD thesis, Department of Computer Science, Technical University of Denmark, 1994."},{"key":"CR17","unstructured":"David E. Muller, ?Asynchronous logics and application to information processing,? in H. Aiken and W.F. Main, editors,Proc. Symp. on Application of Switching Theory in Space Technology, Stanford University Press, 1963, pp. 289?397."},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen Staunstrup,A Formal Approach to Hardware Design, Kluwer Academic Publishers, 1994.","DOI":"10.1007\/978-1-4615-2764-0"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"John P. Van Tassel, ?A formalisation of the VHDL simulation cycle,? in L.J.M. Claesen and M.J.C. Gordon, editors,Higher Order Logic Theorem Proving and its Applications, Vol. IFIP Transactions A-20, Elsevier, 1993, pp. 359?374.","DOI":"10.1016\/B978-0-444-89880-7.50029-2"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384501.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384501\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T04:08:46Z","timestamp":1735531726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,6]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,6]]}},"alternative-id":["BF01384501"],"URL":"https:\/\/doi.org\/10.1007\/bf01384501","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1995,6]]}}}