{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T23:37:42Z","timestamp":1770334662706,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540603856","type":"print"},{"value":"9783540455165","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60385-9_15","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:23:46Z","timestamp":1330280626000},"page":"246-260","source":"Crossref","is-referenced-by-count":7,"title":["Verifying hardware components with JACK"],"prefix":"10.1007","author":[{"given":"R.","family":"Nicola","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Larosa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ristori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"15_CR1","volume-title":"LNCS 663","author":"A. Bouali","year":"1992","unstructured":"A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Fourth Workshop on Computer-Aided Verification, Montreal, 1992, LNCS 663, Springer-Verlag."},{"key":"15_CR2","first-page":"207","volume":"n.54","author":"A. Bouali","year":"1994","unstructured":"A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n.54, October 1994, pp. 207\u2013223.","journal-title":"Bulletin of the EATCS"},{"issue":"2","key":"15_CR3","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, A.P. Sistla: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications, ACM Toplas, 8 (2), 1986, pp. 244\u2013263.","journal-title":"ACM Toplas"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Automatic Verification Methods for Finite State Systems, LNCS 407, Springer-Verlag, 1989, pp. 24\u201337.","DOI":"10.1007\/3-540-52148-8_3"},{"key":"15_CR5","unstructured":"M. Danelutto, G. DiCaprio, and A. Masini. Parallelizing a Model Checker. submitted for publication, 1995."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"N. De Francesco, A. Fantechi, S. Gnesi, P. Inverardi. Model Checking of non-finite state processes by Finite Approximations. TACAS Workshop, LNCS, Springer-Verlag. May 1994.","DOI":"10.1007\/3-540-60630-0_10"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Network and ISDN systems, Vol. 25, No.7, North Holland, 1993, pp. 761\u2013778.","DOI":"10.1016\/0169-7552(93)90047-8"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"R. De Nicola, P. Inverardi, and M. Nesi. Equational reasoning about LOTOS specifications: A rewriting approach. In Sixth International Workshop on Software Specification and Design, 1991, pp. 54\u201367.","DOI":"10.1109\/IWSSD.1991.213066"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F.W. Vaandrager. Action versus state based logics for transition systems. In I. Guessarian, editor, Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, Springer-Verlag, 1990, pp. 407\u2013419.","DOI":"10.1007\/3-540-53479-2_17"},{"issue":"N.2","key":"15_CR10","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"R. De Nicola and F.W. Vaandrager. Three Logics for Branching Bisimulation. Journal of ACM, Vol. 42, N. 2, 1995, pp. 458\u2013487.","journal-title":"Journal of ACM"},{"issue":"1","key":"15_CR11","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson, J. Y. Halpern. \u201dSometimes\u201d and \u201dNot Never\u201d Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM, 33 (1),1986, pp. 151\u2013178.","journal-title":"Journal of ACM"},{"issue":"2","key":"15_CR12","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF01384048","volume":"4","author":"A. Fantechi","year":"1994","unstructured":"A. Fantechi, S. Gnesi, G. Ristori, M. Carenini, M. Vanocchi, and P. Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods in Systems Design, 4(2), Elsevier Science Publisher, 1994, pp. 243\u2013263.","journal-title":"Formal Methods in Systems Design"},{"key":"15_CR13","unstructured":"G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4\u201347 December 1994."},{"key":"15_CR14","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32, 1985, pp. 137\u2013161.","journal-title":"Journal of ACM"},{"key":"15_CR15","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, London, 1985."},{"key":"15_CR16","unstructured":"P. Inverardi, C. Priami, and D. Yankelevich. Verifing concurrent systems in SML. In SIGPLAN ML Workshop, San Francisco, June 1992."},{"key":"15_CR17","unstructured":"E. Madelaine and R. De Simone. The fc2 reference manual. Technical report, INRIA, 1993."},{"key":"15_CR18","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989."},{"key":"15_CR19","first-page":"65","volume-title":"LNCS 531","author":"V. Roy","year":"1990","unstructured":"V. Roy and R. de Simone. AUTO and autograph. In R. Kurshan, editor, Workshop on Computer Aided Verification, New-Brunswick, June 1990. LNCS 531, Springer-Verlag, pp. 65\u201375."}],"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_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:58:53Z","timestamp":1605646733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}