{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214736},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417682"},{"type":"electronic","value":"9783540452416"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45241-9_2","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T14:24:00Z","timestamp":1188311040000},"page":"14-28","source":"Crossref","is-referenced-by-count":12,"title":["Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,29]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"Reachability analysis of (timed) petri nets using real arithmetic","author":"B. B\u00e9rard","year":"1999","unstructured":"B. B\u00e9rard and L. Fribourg. Reachability analysis of (timed) petri nets using real arithmetic. In Proceedings of Concur\u201999, LNCS 1664, pages 178\u2013193. Springer-Verlag, 1999."},{"key":"2_CR3","unstructured":"J. Bowen. Animating the semantics of VERILOG using Prolog. Technical Report UNU\/IIST Technical Report no. 176, United Nations University, Macau, 1999."},{"key":"2_CR4","unstructured":"M. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing. To appear."},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/BFb0056614","volume-title":"Architecturing software using: A methodology for language development","author":"C. Consel","year":"1998","unstructured":"C. Consel and R. Marlet. Architecturing software using: A methodology for language development. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Proceedings of ALP\/PLILP\u201998, LNCS 1490, pages 170\u2013194. Springer-Verlag, 1998."},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Logic programming and model checking","author":"B. Cui","year":"1998","unstructured":"B. Cui, Y. Dong, X. Du, N. Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D. S. Warren. Logic programming and model checking. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Proceedings of ALP\/PLILP\u201998, LNCS 1490, pages 1\u201320. Springer-Verlag, 1998."},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Model checking in clp","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in clp. In R. Cleaveland, editor, Proceedings of TACAS\u201999, LNCS 1579, pages 223\u2013239. Springer-Verlag, 1999."},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","first-page":"61","volume-title":"A process compensation language","author":"C. Ferreira","year":"2000","unstructured":"C. Ferreira and M. Butler. A process compensation language. In Proceedings IFM\u20192000, LNCS 1945, pages 61\u201376. Springer-Verlag, 2000."},{"key":"2_CR9","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 User Manual."},{"key":"2_CR10","unstructured":"J. Gallagher. A system for specialising logic programs. Technical Report TR-91-32, University of Bristol, November 1991."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"G. Gupta. Horn logic denotations and their applications. In The Logic Programming Paradigm: A 25 year perspective, pages 127\u2013160. Springer-Verlag, April 1998.","DOI":"10.1007\/978-3-642-60085-2_6"},{"issue":"3","key":"2_CR12","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF03037481","volume":"16","author":"S. Haridi","year":"1998","unstructured":"S. Haridi, P. Van Roy, P. Brand, and C. Schulte. Programming languages for distributed applications. New Generation Computing, 16(3):223\u2013261, 1998.","journal-title":"New Generation Computing"},{"key":"2_CR13","unstructured":"P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters. Questions and answers about ten formal methods. Technical report, Trento, Italy, July 1999. Extended version as technical report DSSE-TR-99-1, University of Southampton."},{"key":"2_CR14","unstructured":"P. Henderson. Modelling architectures for dynamic systems. Technical report, University of Southampton, December 1999. Available at http:\/\/www.ecs.soton.ac.uk\/~ph\/arc.htm ."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"2_CR16","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyzer. In Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337616"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-61580-6_12","volume-title":"Partial Evaluation, International Seminar","author":"J. J\u00f8rgensen","year":"1996","unstructured":"J. J\u00f8rgensen and M. Leuschel. Efficiently generating efficient generating extensions in Prolog. In O. Danvy, R. Gl\u00fcck, and P. Thiemann, editors, Partial Evaluation, International Seminar, LNCS 1110, pages 238\u2013262, Schlo\u00df Dagstuhl, 1996. Springer-Verlag."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"L. King, G. Gupta, and E. Pontelli. Verification of Bart controller: An approach based on horn logic and denotational semantics. submitted, 2000.","DOI":"10.1007\/978-1-4615-1391-9_11"},{"key":"2_CR20","unstructured":"R. S. Lazic. A semantic study of data-independence with applications to the mechanical verification of concurrent systems. PhD thesis, Oxford University, 1997."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"M. Leuschel and H. Lehmann. Solving coverability problems of Petri nets by partial deduction. In M. Gabbrielli and F. Pfenning, editors, Proceedings of PPDP\u20192000, pages 268\u2013279. ACM Press, 2000.","DOI":"10.1145\/351268.351298"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1145\/271510.271525","volume":"20","author":"M. Leuschel","year":"1998","unstructured":"M. Leuschel, B. Martens, and D. De Schreye. Controlling generalisation and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems, 20(1):208\u2013258, January 1998.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/10720327_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"2000","unstructured":"M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR\u201999, LNCS 1817, pages 63\u201382, Venice, Italy, September 1999."},{"key":"2_CR24","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. L\u00fcbcke. Constraint logic programming for local and symbolic model checking. In J. Lloyd, editor, Proceedings of CL\u20192000, LNAI 1861, pages 384\u2013398, London, UK, 2000. Springer-Verlag.","DOI":"10.1007\/3-540-44957-4_26"},{"key":"2_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-49727-7_15","volume-title":"Static Analysis","author":"J. C. Peralta","year":"1998","unstructured":"J. C. Peralta, J. P. Gallagher, and H. Saglam. Analysis of imperative programs through analysis of constraint logic programs. In G. Levi, editor, Static Analysis. Proceedings of SAS\u201998, LNCS 1503, pages 246\u2013261, Pisa, Italy, September 1998. Springer-Verlag."},{"key":"2_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Efficient model checking using tabled resolution","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In O. Grumberg, editor, Proceedings of CAV\u201997, LNCS 1254, pages 143\u2013154. Springer-Verlag, 1997."},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In IEEE Symposium on Foundations of Secure Systems, 1995.","DOI":"10.1109\/CSFW.1995.518556"},{"key":"2_CR29","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999."},{"issue":"1","key":"2_CR30","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF03038271","volume":"12","author":"D. Sahlin","year":"1993","unstructured":"D. Sahlin. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing, 12(1):7\u201351, 1993.","journal-title":"New Generation Computing"},{"key":"2_CR31","unstructured":"J. B. Scattergood. Tools for CSP and Timed-CSP. PhD thesis, Oxford University, 1997."},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1145\/72551.72555","volume":"21","author":"E. Shapiro","year":"1989","unstructured":"E. Shapiro. The family of concurrent logic programming languages. ACM Computing Surveys, 21(3):413\u2013510, 1989.","journal-title":"ACM Computing Surveys"},{"key":"2_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BFb0015252","volume-title":"Computer Science Today","author":"G. Smolka","year":"1995","unstructured":"G. Smolka. The Oz programming model. In J. van Leeuwen, editor, Computer Science Today, LNCS 1000, pages 324\u2013343. Springer-Verlag, Berlin, 1995."}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45241-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:08:32Z","timestamp":1556816912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45241-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417682","9783540452416"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-45241-9_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}