{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:12:05Z","timestamp":1725520325375},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_18","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T14:56:21Z","timestamp":1224255381000},"page":"278-297","source":"Crossref","is-referenced-by-count":24,"title":["Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[]},{"given":"Marc","family":"Fontaine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J.-R. Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/1229285.1229299","volume-title":"ASIACCS","author":"D.A. Basin","year":"2007","unstructured":"Basin, D.A., Olderog, E.-R., Sevin\u00e7, P.E.: Specifying and analyzing security automata using csp-oz. In: Bao, F., Miller, S. (eds.) ASIACCS, pp. 70\u201381. ACM, New York (2007)"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M. Butler","year":"2000","unstructured":"Butler, M.: csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing\u00a012, 182\u2013198 (2000)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Rigorous Development of Complex Fault-Tolerant Systems","year":"2006","unstructured":"Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol.\u00a04157. Springer, Heidelberg (2006)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11526841_16","volume-title":"FM 2005: Formal Methods","author":"M. Butler","year":"2005","unstructured":"Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 221\u2013236. Springer, Heidelberg (2005)"},{"key":"18_CR6","unstructured":"Fontaine, M., Leuschel, M.: Typechecking csp specifications using haskell (extended abstract). In: Proceedings Avocs 2007, Oxford, UK, pp. 171\u2013176 (2007)"},{"key":"18_CR7","unstructured":"Formal\u00a0Systems\u00a0(Europe)\u00a0Ltd. Failures-Divergence Refinement \u2014 FDR2 User Manual (version 2.8.2)"},{"key":"18_CR8","unstructured":"Formal\u00a0Systems\u00a0(Europe)\u00a0Ltd. Process Behaviour Explorer (ProBE User Manual, version 1.30), http:\/\/www.fsel.com\/probe_manual.html"},{"key":"18_CR9","first-page":"421","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"P. Hill","year":"1998","unstructured":"Hill, P., Gallagher, J.: Meta-programming in logic programming. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a05, pp. 421\u2013497. Oxford Science Publications, Oxford University Press, Oxford (1998)"},{"key":"18_CR10","volume-title":"Communicating Sequential Processes","author":"C. Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"18_CR11","unstructured":"Hutton, G., Meijer, E.: Monadic Parser Combinators. Technical Report NOTTCS-TR-96-4, Department of Computer Science, University of Nottingham (1996)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-31980-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Isobe","year":"2005","unstructured":"Isobe, Y., Roggenbach, M.: A generic theorem prover of CSP refinement. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 108\u2013123. Springer, Heidelberg (2005)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_37","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Johnsson","year":"1985","unstructured":"Johnsson, T.: Lambda lifting: Transforming programs to recursive equations. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201. Springer, Heidelberg (1985)"},{"key":"18_CR14","volume-title":"The Implementation of Functional Programming Languages","author":"S.P. Jones","year":"1987","unstructured":"Jones, S.P.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-45241-9_2","volume-title":"Practical Aspects of Declarative Languages","author":"M. Leuschel","year":"2001","unstructured":"Leuschel, M.: Design and implementation of the high-level specification language CSP(LP) in Prolog. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol.\u00a01990, pp. 14\u201328. Springer, Heidelberg (2001)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11576280_24","volume-title":"Formal Methods and Software Engineering","author":"M. Leuschel","year":"2005","unstructured":"Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 345\u2013359. Springer, Heidelberg (2005)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/11955757_9","volume-title":"B 2007: Formal Specification and Development in B","author":"M. Leuschel","year":"2006","unstructured":"Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 79\u201393. Springer, Heidelberg (2006)"},{"key":"18_CR19","unstructured":"Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proceedings International Symmetry Conference, Edinburgh, UK, January 2007, pp. 71\u201385 (2007)"},{"key":"18_CR20","unstructured":"Leuschel, M., Plagge, D.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In: Ameur, Y.A., Boniol, F., Wiels, V. (eds.) Proceedings Isola 2007. Revue des Nouvelles Technologies de l\u2019Information, vol.\u00a0RNTI-SM-1, C\u00e9padu\u00e8s-\u00c9ditions (2007)"},{"issue":"1-2","key":"18_CR21","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security\u00a06(1-2), 53\u201384 (1998)","journal-title":"Journal of Computer Security"},{"key":"18_CR22","unstructured":"Naish, L.: An introduction to MU-Prolog. Technical Report 82\/2, Department of Computer Science, University of Melbourne, Melbourne, Australia, March 1982 (Revised, July 1983)"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Computer Aided Verification","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 143\u2013154. Springer, Heidelberg (1997)"},{"key":"18_CR24","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1999","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1999)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking csp or how to check 10 $^{\\mbox{20}}$ dining philosophers for deadlock. In: TACAS 2005, pp. 133\u2013152 (1995)","DOI":"10.1007\/3-540-60630-0_7"},{"key":"18_CR26","unstructured":"Scattergood, J.B.: Tools for CSP and Timed-CSP. PhD thesis, Oxford University (1997)"},{"key":"18_CR27","volume-title":"Concurrent and Real-time Systems: The CSP Approach","author":"S. Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. Wiley, Chichester (1999)"},{"key":"18_CR28","unstructured":"Steria, F.: Aix-en-Provence. Atelier B, User and Reference Manuals (1996), http:\/\/www.atelierb.societe.com"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-44525-0_12","volume-title":"ZB 2000: Formal Specification and Development in Z and B","author":"H. Treharne","year":"2000","unstructured":"Treharne, H., Schneider, S.: How to drive a B machine. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol.\u00a01878, pp. 188\u2013208. Springer, Heidelberg (2000)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44880-2_5","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"H. Treharne","year":"2003","unstructured":"Treharne, H., Schneider, S., Bramble, M.: Composing specifications using communication. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M.A. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 58\u201378. Springer, Heidelberg (2003)"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11526841_17","volume-title":"FM 2005: Formal Methods","author":"J. Woodcock","year":"2005","unstructured":"Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 237\u2013252. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T19:08:07Z","timestamp":1557860887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}