FDR3

FDR3 — A Modern Refinement Checker for CSP. FDR3 is a complete rewrite of the CSP refinement checker FDR2, incorporating a significant number of enhancements. In this paper we describe the operation of FDR3 at a high level and then give a detailed description of several of its more important innovations. This includes the new multi-core refinement-checking algorithm that is able to achieve a near linear speed up as the number of cores increase. Further, we describe the new algorithm that FDR3 uses to construct its internal representation of CSP processes—this algorithm is more efficient than FDR2’s, and is able to compile a large class of CSP processes to more efficient internal representations. We also present experimental results that compare FDR3 to related tools, which show it is unique (as far as we know) in being able to scale beyond the bounds of main memory


References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Antonino, Pedro; Gibson-Robinson, Thomas; Roscoe, A. W.: Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving (2019)
  2. Llorens, M.; Oliver, J.; Silva, J.; Tamarit, S.: Tracking CSP computations (2019)
  3. Lowe, Gavin: Discovering and correcting a deadlock in a channel implementation (2019)
  4. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  5. van Glabbeek, Rob: Ensuring liveness properties of distributed systems: open problems (2019)
  6. Cleaveland, Rance; Roscoe, A. W.; Smolka, Scott A.: Process algebra and model checking (2018)
  7. Conserva Filho, M. S.; Oliveira, M. V. M.; Sampaio, A.; Cavalcanti, Ana: Compositional and local livelock analysis for CSP (2018)
  8. Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
  9. Pedersen, Jan B.; Welch, Peter H.: The symbiosis of concurrency and verification: teaching and case studies (2018)
  10. Dalsgaard, Andreas E.; Enevoldsen, Søren; Fogh, Peter; Jensen, Lasse S.; Jepsen, Tobias S.; Kaufmann, Isabella; Larsen, Kim G.; Nielsen, Søren M.; Olesen, Mads Chr.; Pastva, Samuel; Srba, Jiří: Extended dependency graphs and efficient distributed fixed-point computation (2017)
  11. Boulgakov, Alexandre; Gibson-Robinson, Thomas; Roscoe, A. W.: Computing maximal weak and other bisimulations (2016)
  12. Cavalcanti, Ana; Woodcock, Jim; Amálio, Nuno: Behavioural models for FMI co-simulations (2016)
  13. Jähnig, Nils; Göthel, Thomas; Glesner, Sabine: Refinement-based verification of communicating unstructured code (2016)
  14. Mestel, David; Roscoe, A. W.: Reducing complex CSP models to traces via priority (2016)
  15. Oliveira, Marcel V. M.; Antonino, P.; Ramos, R.; Sampaio, A.; Mota, A.; Roscoe, A. W.: Rigorous development of component-based systems using component metadata and patterns (2016)
  16. Garavel, Hubert: Revisiting sequential composition in process calculi (2015)
  17. Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
  18. Roscoe, A. W.: The expressiveness of CSP with priority (2015)
  19. Gibson-Robinson, Thomas; Armstrong, Philip; Boulgakov, Alexandre; Roscoe, Andrew W.: FDR3 -- a modern refinement checker for CSP (2014)
  20. Li, Liyi; Gunter, Elsa; Mansky, William: Symbolic analysis tools for CSP (2014)