{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:45Z","timestamp":1725631965179},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105395","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"33-50","source":"Crossref","is-referenced-by-count":3,"title":["Modeling a hardware synthesis methodology in isabelle"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Friedrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"3_CR1","unstructured":"David A. Basin. Logic frameworks for logic programs. In 4th International Workshop on Logic Program Synthesis and Transformation, (LOPSTR'94), volume 883 of LNCS, pages 1\u201316, Pisa Italy, June 1994. Springer-Verlag."},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"David A. Basin and Nils Klarlund. Hardware verification using monadic second-order logic. In Computer-Aided Verification (CAV\u2019 95), volume 939 of LNCS, pages 31\u201341. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_38"},{"key":"3_CR3","unstructured":"A. J. Camilleri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986."},{"key":"3_CR4","series-title":"Technical Report","volume-title":"Interactive program derivation","author":"M. D. Coen","year":"1992","unstructured":"Martin David Coen. Interactive program derivation. Technical Report 272, Cambridge University Computer Laboratory, Cambridge, November 1992."},{"key":"3_CR5","unstructured":"S. Finn, M. P. Fourman, M. Francis, and R. Harris. Formal system design \u2014 interactive synthesis based on computer-assisted formal reasoning. In Dr. Luc Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, volume 1, pages 97\u2013110, Amsterdam, 1989. Elsevier Science publishers B.V. (North-Holland)."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Cordell Green. Application of theorem proving to problem solving. In Proceedings of the IJCAI-69, pages 219\u2013239, 1969.","DOI":"10.21236\/ADA459656"},{"key":"3_CR7","unstructured":"F. Keith Hanna, Neil Daeche, and Mark Longley. Formal synthesis of digital systems. In IMEC-IFIP International Workshop on: Applied Formal Methods For Correct VLSI Design, volume 2, pages 532\u2013548, Leuven, Belgium, 1989."},{"key":"3_CR8","volume-title":"Handware Specification, Verification and Synthesis: Mathematical Aspects","author":"F.K. Hanna","year":"1989","unstructured":"F.K. Hanna, N. Daeche, and M. Longley. VERITAS+: A specification language based on type theory. In Handware Specification, Verification and Synthesis: Mathematical Aspects, Ithaca, New York, 1989, Springer-Verlag."},{"key":"3_CR9","unstructured":"John L. Hennessy and David A. Patterson. Computer Architecture, a Quantitative Approach. Morgan Kaufmann, 1990."},{"key":"3_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover; with contributions by Tobias Nipkow, volume 828 of LNCS","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: a generic theorem prover; with contributions by Tobias Nipkow, volume 828 of LNCS. Springer, Berlin, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105395","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:44:43Z","timestamp":1560937483000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105395"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0105395","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}