{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:34:51Z","timestamp":1784932491479,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548611","type":"print"},{"value":"9783642548628","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_13","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:33:34Z","timestamp":1395394414000},"page":"187-201","source":"Crossref","is-referenced-by-count":169,"title":["FDR3 \u2014 A Modern Refinement Checker for CSP"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Gibson-Robinson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Armstrong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Boulgakov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River (1985)"},{"key":"13_CR2","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1997)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer (2010)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11423348_9","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"J. Lawrence","year":"2005","unstructured":"Lawrence, J.: Practical Application of CSP and FDR to Software Design. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP25. LNCS, vol.\u00a03525, pp. 151\u2013174. Springer, Heidelberg (2005)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming\u00a040(1) (2001)","DOI":"10.1016\/S0167-6423(00)00023-X"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-Checking CSP-OZ Specifications with FDR. In: IFM 1999. Springer (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: A Compiler for the Analysis of Security Protocols. Journal of Computer Security\u00a06(1-2) (1998)","DOI":"10.3233\/JCS-1998-61-204"},{"key":"13_CR8","unstructured":"Roscoe, A.W., Hopkins, D.: SVA, a Tool for Analysing Shared-Variable Programs. In: Proceedings of AVoCS 2007 (2007)"},{"key":"13_CR9","unstructured":"Holzmann, G.: Spin Model Checker: The Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2013","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., Ro\u010dkai, P., \u0160till, V., Weiser, J.: DiVinE 3.0 \u2013 An Explicit-State Model Checker for Multithreaded C & C++ Programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-642-20398-5_40","volume-title":"NASA Formal Methods","author":"A. Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Multi-Core LTSmin: Marrying Modularity and Scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 506\u2013511. Springer, Heidelberg (2011)"},{"key":"13_CR12","unstructured":"University of Oxford, Failures-Divergence Refinement\u2014FDR\u00a03 User Manual (2013), \n                    \n                      https:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/"},{"key":"13_CR13","unstructured":"University of Oxford, libcspm (2013), \n                    \n                      https:\/\/github.com\/tomgr\/libcspm"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Reed, G.M., Roscoe, A.W.: A Timed Model for Communicating Sequential Processes. Theoretical Computer Science\u00a058 (1988)","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"13_CR15","unstructured":"Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking Timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)"},{"key":"13_CR16","unstructured":"Ouaknine, J.: Discrete Analysis of Continuous Behaviour in Real-Time Concurrent Systems. DPhil Thesis (2001)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM (1986)","DOI":"10.1145\/512644.512660"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-39698-4_20","volume-title":"Theories of Programming and Formal Methods","author":"A.W. Roscoe","year":"2013","unstructured":"Roscoe, A.W., Hopcroft, P.J.: Slow abstraction via priority. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol.\u00a08051, pp. 326\u2013345. Springer, Heidelberg (2013)"},{"key":"13_CR19","unstructured":"Roscoe, A.W.: Model-Checking CSP. In: A Classical Mind: Essays in Honour of CAR Hoare (1994)"},{"key":"13_CR20","unstructured":"Goldsmith, M., Martin, J.: The parallelisation of FDR. In: Proceedings of the Workshop on Parallel and Distributed Model Checking (2002)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Leiserson, C.E., Schardl, T.B.: A work-efficient parallel breadth-first search algorithm (or how to cope with the nondeterminism of reducers). In: Proc. 22nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2010 (2010)","DOI":"10.1145\/1810479.1810534"},{"key":"13_CR22","unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: Proc. 20th National Conference on Artificial Intelligence, vol.\u00a03. AAAI (2005)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31759-0_12","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2012","unstructured":"Holzmann, G.J.: Parallelizing the Spin Model Checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 155\u2013171. Springer, Heidelberg (2012)"},{"key":"13_CR24","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Formal Methods in Computer-Aided Design (2010)"}],"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\/978-3-642-54862-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:59:09Z","timestamp":1558857549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}