{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T00:54:42Z","timestamp":1783990482274,"version":"3.55.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,4,5]],"date-time":"2015-04-05T00:00:00Z","timestamp":1428192000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10009-015-0377-y","type":"journal-article","created":{"date-parts":[[2015,4,4]],"date-time":"2015-04-04T08:19:53Z","timestamp":1428135593000},"page":"149-167","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["FDR3: a parallel refinement checker for CSP"],"prefix":"10.1007","volume":"18","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":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,4,5]]},"reference":[{"key":"377_CR1","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River (1985)"},{"key":"377_CR2","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, New Jersey (1997)"},{"key":"377_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, New York (2010)"},{"key":"377_CR4","unstructured":"Formal Systems (Europe) Ltd.: Failures-Divergence Refinement\u2013FDR 2 User Manual, (2011)"},{"key":"377_CR5","doi-asserted-by":"crossref","unstructured":"Goldsmith, M.: Operational Semantics for Fun and Profit. In: Communicating Sequential Processes. The First 25 Years, vol. 3525 of LNCS (2005)","DOI":"10.1007\/11423348_16"},{"key":"377_CR6","doi-asserted-by":"crossref","unstructured":"Lawrence, J.: Practical Application of CSP and FDR to Software Design. In: Communicating Sequential Processes. The First 25 Years, vol. 3525 of LNCS (2005)","DOI":"10.1007\/11423348_9"},{"issue":"1","key":"377_CR7","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A Mota","year":"2001","unstructured":"Mota, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Sci. Comput. Program. 40(1), 59\u201396 (2001)","journal-title":"Sci. Comput. Program."},{"key":"377_CR8","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: IFM\u201999. Springer, New York (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"issue":"1\u2014-2","key":"377_CR9","doi-asserted-by":"crossref","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. J. Comput. Secur. 6(1\u2014-2), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"key":"377_CR10","unstructured":"Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. In: Proceedings of AVoCS 2007 (2007)"},{"key":"377_CR11","volume-title":"Spin Model Checker: The Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin Model Checker: The Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"377_CR12","doi-asserted-by":"crossref","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: an explicit-state model checker for multithreaded C & C++ Programs. In: CAV, vol. 8044 of LNCS (2013)","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"377_CR13","doi-asserted-by":"crossref","unstructured":"Laarman, A., Pol, J.V.D., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: NASA Formal Methods, vol. 6617 of LNCS (2011)","DOI":"10.1007\/978-3-642-20398-5_40"},{"key":"377_CR14","doi-asserted-by":"crossref","unstructured":"Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal bisimulations. In: Formal Methods and Software Engineering, vol. 8829 of LNCS (2014)","DOI":"10.1007\/978-3-319-11737-9_2"},{"key":"377_CR15","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Roscoe, A.W., Hansen, H., Wang, X.: Practical partial order reduction for CSP. In: NASA Formal Methods (2015)","DOI":"10.1007\/978-3-319-17524-9_14"},{"key":"377_CR16","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a modern model checker for CSP. In: TACAS, vol. 8413 of LNCS (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"377_CR17","unstructured":"Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In: Communicating Process Architectures (2014)"},{"key":"377_CR18","unstructured":"University of Oxford, libcspm. https:\/\/github.com\/tomgr\/libcspm (2013)"},{"key":"377_CR19","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"GM Reed","year":"1988","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58, 249\u2013261 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"377_CR20","unstructured":"Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)"},{"key":"377_CR21","unstructured":"Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. DPhil Thesis (2001)"},{"key":"377_CR22","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, New York (1986)","DOI":"10.1145\/512644.512660"},{"key":"377_CR23","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Hopcroft, P.J.: Slow abstraction via priority. In: Theories of Programming and Formal Methods, vol. 8051 of LNCS (2013)","DOI":"10.1007\/978-3-642-39698-4_20"},{"key":"377_CR24","unstructured":"Roscoe, A.W.: Model-checking CSP. A Classical Mind: Essays in Honour of CAR Hoare (1994)"},{"key":"377_CR25","unstructured":"Goldsmith, M., Martin, J.: The parallelisation of FDR. In: Proceedings of the Workshop on Parallel and Distributed Model Checking (2002)"},{"key":"377_CR26","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 (2010)","DOI":"10.1145\/1810479.1810534"},{"key":"377_CR27","unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: Proc. 20th National Conference on Artificial Intelligence, vol. 3, AAAI (2005)"},{"key":"377_CR28","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Parallelizing the spin model checker. In: Model Checking Software, vol. 7385 of LNCS (2012)","DOI":"10.1007\/978-3-642-31759-0_12"},{"key":"377_CR29","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)"},{"key":"377_CR30","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Simecek, P.: Cluster-based I\/O-efficient LTL model checking. In: ASE, pp. 635\u2013639. IEEE (2009)","DOI":"10.1109\/ASE.2009.32"},{"key":"377_CR31","doi-asserted-by":"crossref","unstructured":"Verstoep, K., Bal, H.E., Barnat, J., Brim, L.: Efficient large-scale model checking. In: IPDPS, pp. 1\u201312. IEEE (2009)","DOI":"10.1109\/IPDPS.2009.5161000"},{"key":"377_CR32","unstructured":"Hughes, J.: Graph reduction with super-combinators. Tech. Rep. PRG28, OUCL (1982)"},{"issue":"2","key":"377_CR33","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Softw. Tools Technol. Transf. (STTT) 10(2), 185\u2013203 (2008)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"377_CR34","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: Pat: Towards flexible verification under fairness, vol. 5643 of Lecture Notes in Computer Science, pp. 709\u2013714. Springer, New York (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"377_CR35","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Concurrent depth-first search algorithms. In: TACAS, pp. 202\u2013216 (2014)","DOI":"10.1007\/978-3-642-54862-8_14"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0377-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0377-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0377-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T22:54:54Z","timestamp":1566514494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0377-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,5]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["377"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0377-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,5]]}}}