DIVINE is a tool for LTL model checking and reachability analysis of discrete distributed systems. The tool is able to efficiently exploit the aggregate computing power of multiple network-interconnected multi-cored workstations in order to deal with extremely large verification tasks. As such it allows to analyse systems whose size is far beyond the size of systems that can be handled with regular sequential tools.

References in zbMATH (referenced in 29 articles )

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

1 2 next

  1. Barnat, Jiří; Bauch, Petr; Beneš, Nikola; Brim, Luboš; Beran, Jan; Kratochvíla, Tomáš: Analysing sanity of requirements for avionics systems (2016)
  2. Bérard, Béatrice; Lafourcade, Pascal; Millet, Laure; Potop-Butucaru, Maria; Thierry-Mieg, Yann; Tixeuil, Sébastien: Formal verification of mobile robot protocols (2016)
  3. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  4. Barnat, Jiří: Quo vadis explicit-state model checking (2015)
  5. Cranen, Sjoerd; Groote, Jan Friso; Keiren, Jeroen J.A.; Stappers, Frank P.M.; de Vink, Erik P.; Wesselink, Wieger; Willemse, Tim A.C.: An overview of the mCRL2 toolset and its recent advances (2013)
  6. Lamo, Yngve; Wang, Xiaoliang; Mantz, Florian; Bech, Øyvind; Sandven, Anders; Rutle, Adrian: DPF workbench: a multi-level language workbench for MDE (2013) ioport
  7. Babiak, Tomáš; Řehák, Vojtěch; Strejček, Jan: Almost linear Büchi automata (2012)
  8. Barnat, Jiří; Bauch, Petr; Brim, Luboš; Češka, Milan: Designing fast LTL model checking algorithms for many-core GPUs (2012) ioport
  9. Barnat, Jiri; Beran, Jan; Brim, Lubos; Kratochvíla, Tomas; Ročkai, Petr: Tool chain to support automated formal verification of avionics simulink designs (2012) ioport
  10. Barnat, Jiří; Brim, Luboš; Ročkai, Petr: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties (2012)
  11. Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jaco: Improved multi-core nested depth-first search (2012)
  12. Barnat, Jiří; Chaloupka, Jakub; van de Pol, Jaco: Distributed algorithms for SCC decomposition (2011)
  13. Bauch, Petr; Češka, Milan: CUDA accelerated LTL model checking -- revisited (2011)
  14. Beneš, N.; Brim, L.; Buhnova, B.; Černá, I.; Sochor, J.; Vařeková, P.: Partial order reduction for state/event LTL with application to component-interaction automata (2011)
  15. Edelkamp, S.; Sulewski, D.; Barnat, J.; Brim, L.; Šimeček, P.: Flash memory efficient LTL model checking (2011)
  16. Edelkamp, Stefan; Sulewski, Damian: External memory breadth-first search with delayed duplicate detection on the GPU (2011) ioport
  17. Evangelista, Sami; Petrucci, Laure; Youcef, Samir: Parallel nested depth-first searches for LTL model checking (2011)
  18. Laarman, Alfons; Langerak, Rom; van de Pol, Jaco; Weber, Michael; Wijs, Anton: Multi-core nested depth-first search (2011)
  19. Schlacher, Kurt (ed.); Schöberl, Markus (ed.): Part special issue: Modelling analysis and control of distributed parameter systems. Selected papers based on the presentations at the 6th MATHMOD conference, Vienna, Austria, February 2009 (2011)
  20. Evangelista, Sami; Kristensen, Lars Michael: Search-order independent state caching (2010)

1 2 next

Further publications can be found at: http://divine.fi.muni.cz/papers.html