{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:22Z","timestamp":1725664402523},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603856"},{"type":"electronic","value":"9783540455165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60385-9_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:23:56Z","timestamp":1330280636000},"page":"225-245","source":"Crossref","is-referenced-by-count":2,"title":["Formal support for the ELLA hardware description language"],"prefix":"10.1007","author":[{"given":"Howard","family":"Barringer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham","family":"Gough","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Monahan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Williams","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"14_CR1","unstructured":"J. D. Morison and A. S. Clarke. ELLA2000: A Language for Electronic System Design. McGraw-Hill, 1993."},{"key":"14_CR2","unstructured":"D. Schmidt. Denotational Semantics. Allyn and Bacon, 1986."},{"key":"14_CR3","unstructured":"H. Barringer, G. Gough, T. Longshaw, B. Monahan, M. Peim, and A. Williams. Semantics and Verification for Boolean Kernel ELLA using IO Automata. In Advanced Research Workshop on Correct Hardware Design Methodologies (CHARME'91), Turin, Italy, May 1991."},{"key":"14_CR4","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"14_CR5","unstructured":"N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A Reference Manual (Beta Release). Technical report, Computer Science Laboratory, SRI International, March 1993."},{"key":"14_CR6","unstructured":"H. Barringer, G. Gough, B. Monahan, and A. Williams. A Process Algebra Foundation for Reasoning about Core ELLA. Technical Report UMCS-94-12-1, University of Manchester, December 1994."},{"key":"14_CR7","unstructured":"H. Barringer, G. Gough, B. Monahan, and A. Williams. A State Evolution Method for Verifying Hardware Systems. Technical Report UMCS-95-7-1, University of Manchester, July 1995. Also to be presented as a poster at CHARME'95, Frankfurt, Germany, October 1995."},{"key":"14_CR8","unstructured":"Computer General Electronic Design, Chippenham, Wiltshire, United Kingdom. The ELLA Language Reference Manual, 5.1 edition, February 1991."},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"D. Coelho. The VHDL Handbook. Kluwer, 1989.","DOI":"10.1007\/978-1-4613-1633-6"},{"key":"14_CR10","unstructured":"N.A. Lynch and M.R. Tuttle. An Introduction to Input\/Output Automata. Technical Report MIT\/LCS\/TM-373, MIT, November 1988."},{"key":"14_CR11","unstructured":"Formal Verification Support for ELLA. Technical report, DRA (Malvern), Harlequin Ltd. (Cambridge), and University of Manchester, Formal Verification Support for ELLA, IED project 4\/1\/1357, in JFIT Conference, December 1992."},{"key":"14_CR12","unstructured":"Harlequin Ltd, Cambridge UK. Information about LispWorks is available on the World-Wide Web, URL: http:\/\/www.harlequin.co.uk\/full\/products\/sp\/lispworks.html."},{"key":"14_CR13","unstructured":"H. Barringer, G. Gough, B. Monahan, and A. Williams. A Semantics for Core ELLA. Project Report D2.3b, Formal Verification Support for ELLA, IED Project 4\/1\/1357, University of Manchester, November 1992."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"14_CR15","unstructured":"G. A. McCaskill and G. Milne. Hardware Description and Verification Using the Circal-System. Technical Report HDV-24-92, Department of Computer Science, University of Strathclyde, June 1992."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1), 1987.","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"14_CR17","unstructured":"H. Barringer, G.D. Gough, B.Q. Monahan, and A. Williams. A Process Algebraic Semantics for Core ELLA. Technical Report UMCS-93-2-1, University of Manchester, November 1994."},{"key":"14_CR18","unstructured":"H. Barringer, G. Gough, B. Monahan, and A. Williams. The ELLA Verification Environment: A Tutorial Introduction. Technical Report UMCS-94-12-2, University of Manchester, December 1994."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"R. Kumar, K. Schneider, and T. Kropf. Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment. Formal Methods in System Design, 2, 1993.","DOI":"10.1007\/BF01383880"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"M. Gordon and A. Pitts. The HOL logic and system (Chapter 3). In J. Bowen, editor, Towards Verified Systems, pages 49\u201370. Elsevier, October 1994.","DOI":"10.1016\/B978-0-444-89901-9.50012-4"},{"key":"14_CR21","series-title":"LNCS, volume 683","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/BFb0021728","volume-title":"Correct Hardware Design and Verification Methods (CHARME '93)","author":"T. Kropf","year":"1993","unstructured":"T. Kropf, R. Kumar, and K. Schneider. Embedding Hardware Verification within a Commercial Design Framework. In G. Milne and L. Pierre, editors, Correct Hardware Design and Verification Methods (CHARME '93), LNCS, volume 683, pages 242\u2013257, Arles, France, May 1993. Springer-Verlag."},{"key":"14_CR22","volume-title":"CHDL '93","author":"F. Corella","year":"1993","unstructured":"F. Corella. Automated High-Level Verification against Clocked Algorithmic Specifications. In D. Agnew, L. Claesen, and R. Camposano, editors, CHDL '93, Canada, 1993. North-Holland."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"A. Cohn. A Proof of Correctness of the Viper Microprocessor: The First Level. In G. Birtwistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, 1989.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of finite state concurrent systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"14_CR25","series-title":"LNCS, volume 407","volume-title":"Automatic Verification Methods for Finite State Systems","author":"H. Barringer","year":"1989","unstructured":"H. Barringer, M. Fisher, and G.D. Gough. Fair SMG and Linear Time Model Checking. In Sifakis [33]."},{"issue":"8","key":"14_CR26","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long. Representing Circuits More Efficiently in Symbolic Model Checking. In DAC91, 1991.","DOI":"10.1145\/127601.127702"},{"key":"14_CR28","series-title":"LNCS, volume 407","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J-C. Madre. Verification of Synchronous Sequential Machines based on Symbolic Execution. In Sifakis [33]."},{"key":"14_CR29","series-title":"LNCS, volume 697","volume-title":"Computer Aided Verification, (CAV '93)","author":"N. Shankar","year":"1993","unstructured":"N. Shankar. Verification of Real-Time Systems Using PVS. In C. Courcoubetis, editor, Computer Aided Verification, (CAV '93), LNCS, volume 697, Elounda, Greece, June 1993. Springer-Verlag."},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"M. Hennessy and H. Lin. Proof Systems for Message-Passing Process Algebras. Technical Report 5\/93, University of Sussex, 1993.","DOI":"10.1007\/3-540-57208-2_15"},{"key":"14_CR31","unstructured":"K.G.W. Goossens. Embedding Hardware Description Languages in Proof Systems. PhD thesis, University of Edinburgh, 1992."},{"key":"14_CR32","unstructured":"R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. The HOL Verification of ELLA Designs. Technical report, University of Cambridge Computer Laboratory, 1990."},{"key":"14_CR33","series-title":"LNCS, volume 407","volume-title":"Automatic Verification Methods for Finite State Systems","year":"1989","unstructured":"J. Sifakis, editor. Automatic Verification Methods for Finite State Systems, LNCS, volume 407, Grenoble, France, 1989. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60385-9_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:46:54Z","timestamp":1640944014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}