{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:17:05Z","timestamp":1725495425239},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_19","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T16:56:57Z","timestamp":1194973017000},"page":"270-284","source":"Crossref","is-referenced-by-count":5,"title":["Process Algebra in PVS"],"prefix":"10.1007","author":[{"given":"Twan","family":"Basten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jozef","family":"Hooman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"issue":"4","key":"19_CR1","first-page":"257","volume":"4","author":"G. J. Akkerman","year":"1991","unstructured":"G. J. Akkerman and J. C. M. Baeten. Term rewriting analysis in process algebra. CWI Quarterly, 4(4):257\u2013267, 1991.","journal-title":"CWI Quarterly"},{"key":"19_CR2","first-page":"149","volume-title":"Handbook of Logic in Computer Science","author":"J. C. M. Baeten","year":"1995","unstructured":"J. C. M. Baeten and C. Verhoef. Concrete process algebra. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, Semantic Modelling, pages 149\u2013268. Oxford University Press, Oxford, UK, 1995."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"J. C. M. Baeten and W. P. Weijland. Process Algebra. Prentice-Hall, 1990.","DOI":"10.1017\/CBO9780511624193"},{"issue":"4","key":"19_CR4","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1093\/comjnl\/37.4.243","volume":"37","author":"J. A. Bergstra","year":"1994","unstructured":"J. A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration and nesting. The Computer Journal, 37(4):241\u2013258, 1994.","journal-title":"The Computer Journal"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01212523","volume":"9","author":"M. A. Bezem","year":"1997","unstructured":"M. A. Bezem, R. N. Bol, and J. F. Groote. Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects of Computing, 9(1):1\u201348, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"A. Camilleri. A Higher Order Logic mechanization of the CSP failure-divergence semantics. In Proc. IV Higher Order Workshop, pages 123\u2013150. Workshops in Computing, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3182-3_9"},{"key":"19_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/3540539816_72","volume-title":"TAPSOFT\u201991","author":"A. Camilleri","year":"1991","unstructured":"A. Camilleri, P. Inverardi, and M. Nesi. Combining interaction and automation in process algebra verification. In TAPSOFT\u201991, pages 283\u2013296. LNCS 494, Springer-Verlag, 1991."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Gada, P. Lewis, S. Smolka, O. Sokolsky, and S. Zhang. The Concurrency Factory-practical tools for specification, simulation, verification, and implementation. In Proc. DIMACS Workshop on Specification of Parallel Algorithms, 1994.","DOI":"10.1090\/dimacs\/018\/06"},{"key":"19_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/3-540-60117-1_17","volume-title":"Mathematics of Program Construction","author":"R. Groenboom","year":"1995","unstructured":"R. Groenboom, C. Hendriks, I. Polak, J. Terlouw, and J. T. Udding. Algebraic proof assistants in HOL. In Mathematics of Program Construction, pages 304\u2013321. LNCS 947, Springer-Verlag, 1995."},{"key":"19_CR10","series-title":"Computing Science Report","volume-title":"A computer checked algebraic verification of a distributed summation algorithm","author":"J. F. Groote","year":"1997","unstructured":"J. F. Groote, F. Monin, and J. Springintveld. A computer checked algebraic verification of a distributed summation algorithm. Computing Science Report 97\/14, Eindhoven University of Technology, The Netherlands, 1997."},{"key":"19_CR11","first-page":"815","volume":"II","author":"H. Korver","year":"1996","unstructured":"H. Korver and A. Sellink. On automating process algebra proofs. In Proc. Symp. on Computer and Information Sciences, ISCIS XI, volume II, pages 815\u2013826, 1996.","journal-title":"Proc. Symp. on Computer and Information Sciences, ISCIS XI"},{"key":"19_CR12","series-title":"Lect Notes Comput Sci","first-page":"136","volume-title":"Proc. Third Workshop on Computer Aided Verification","author":"H. Lin","year":"1991","unstructured":"H. Lin. PAM: A process algebra manipulator. In Proc. Third Workshop on Computer Aided Verification, pages 136\u2013146. LNCS 575, Springer-Verlag, 1991."},{"key":"19_CR13","series-title":"Lect Notes Comput Sci","first-page":"158","volume-title":"Proc. Third Workshop on Computer Aided Verification","author":"S. Mauw","year":"1991","unstructured":"S. Mauw and G. J. Veltink. A proof assistant for PSF. In Proc. Third Workshop on Computer Aided Verification, pages 158\u2013168. LNCS 575, Springer-Verlag, 1991."},{"key":"19_CR14","unstructured":"T. F. Melham. A mechanized theory of the \u03c0-calculus in HOL. Technical Report 244, Computer Laboratory, University of Cambridge, 1992."},{"key":"19_CR15","series-title":"Lect Notes Comput Sci","first-page":"352","volume-title":"Proc. 6th Workshop on Higher Order Logic Theorem Proving and Applications","author":"M. Nesi","year":"1993","unstructured":"M. Nesi. Value-passing CCS in HOL. In Proc. 6th Workshop on Higher Order Logic Theorem Proving and Applications, pages 352\u2013365. LNCS 780, Springer-Verlag, 1993."},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. LNCS 828, Springer-Verlag, 1994."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,19]],"date-time":"2019-01-19T02:41:46Z","timestamp":1547865706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}