{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:20Z","timestamp":1725664160006},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540576013"},{"type":"electronic","value":"9783540482864"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57601-0_49","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:11:48Z","timestamp":1330261908000},"page":"179-189","source":"Crossref","is-referenced-by-count":1,"title":["Formal methods and their future"],"prefix":"10.1007","author":[{"given":"G.","family":"Musgrave","sequence":"first","affiliation":[]},{"given":"S.","family":"Finn","sequence":"additional","affiliation":[]},{"given":"M.","family":"Francis","sequence":"additional","affiliation":[]},{"given":"R.","family":"Harris","sequence":"additional","affiliation":[]},{"given":"R. B.","family":"Hughes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"14_CR1","unstructured":"R.B. Hughes. Automatic Software Verification and Synthesis. In Proc. 2nd. Int. Conf. on Software Engineering for Real-Time Systems, pages 219\u2013223. Institution of Electrical Engineers, September 1989."},{"key":"14_CR2","unstructured":"E. Mayger and M. Fourman. Integration of formal methods with system design. In A. Halaas and P. B. Denyer, editors, VLSI 91, Edinburgh, Scotland, August 1991."},{"key":"14_CR3","unstructured":"E. Mayger, M. Francis, R. Harris, G. Musgrave, and M. Fourman. The need for a core method. In EUROMICRO 91, September 1991."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"R. B. Hughes, M. D. Francis, S. P. Finn, and G. Musgrave. Formal tools for tri-state design in busses. In Proceedings of the 1992 International Workshop on the HOL Theorem Prover and it Applications, Leuven, Belgium, September 1992.","DOI":"10.1016\/B978-0-444-89880-7.50035-8"},{"key":"14_CR5","unstructured":"D. Shepherd. The role of Occam in the design of the T800. Communicating Process Architecture, pages 93\u2013103, 1988."},{"key":"14_CR6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. Paulson","year":"1987","unstructured":"L. Paulson. Natural deduction proof as higher-order resolution. Logic Programming, 3:237\u2013258, 1987.","journal-title":"Logic Programming"},{"key":"14_CR7","unstructured":"M. Gordon. Why Higher-Order Logic is a good conclusion for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"F.K. Hanna and N. Daeche. Specifications and verification of digital systems using higher-order predicate logic. In IEE Proceedings, volume' 133, 1986. PtE No. 5.","DOI":"10.1049\/ip-e.1986.0031"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Avra Cohn. A proof of correctness of the viper microprocessor: The first level. In Birtwistle and Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"14_CR10","volume-title":"VLSI 89","author":"M. Fourman","year":"1989","unstructured":"M. Fourman and E. Mayger. Formally based system design \u2014 interactive hardware scheduling. In G. Musgrave and U. Lauther, editors, VLSI 89, Munich, Germany, August 1989. Elsevier Science Publishers."},{"key":"14_CR11","unstructured":"R.B. Hughes and R.M. Zimmer. Automated interactive verification of functional programming languages. In C.M.I. Rattray and R.G. Clark, editors, The Unified Computation Laboratory, pages 411\u2013423. Oxford University Press, May 1992."},{"key":"14_CR12","volume-title":"PhD thesis","author":"R. B. Hughes","year":"1992","unstructured":"R. B. Hughes. Automated Interactive Software Verification and Synthesis. PhD thesis, Department of Electrical Engineering and Electronics, Brunel University, Uxbridge, Middx, U.K., July 1992."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"A. Antola and F. Distante. DFG: a graph based approach for algorithmic flow driven architechture synthesis. In Proc. of EUROMICRO 91, Vienna, Austria, September 1991.","DOI":"10.1016\/0165-6074(91)90421-O"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"R. B. Hughes and G. Musgrave. Design-flow graph partitioning. In Proceedings of the 1992 International Workshop on the HOL Theorem Prover and its Applications, Leuven, Belgium, September 1992.","DOI":"10.1016\/B978-0-444-89880-7.50031-0"},{"key":"14_CR15","volume-title":"The Definition of ML","author":"R. Milner","year":"1990","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of ML. The MIT Press, Cambridge, Massachusetts, 1990."},{"key":"14_CR16","unstructured":"M.P. Fourman and Eleanor M. Mayger. Formally based systems design\u2014Interactive hardware scheduling. In VLSI '89. North-Holland, 1989."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory \u2014 EUROCAST '93"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57601-0_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:13:24Z","timestamp":1605647604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57601-0_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540576013","9783540482864"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-57601-0_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}