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 32 articles )

Showing results 1 to 20 of 32.
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. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  6. Wang, Bing; Deng, Bo; Xing, Fei; Wang, Dongxia; Yao, Yiping: Partitioned event graph: formalizing LP-based modelling of parallel discrete-event simulation (2015)
  7. 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)
  8. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  9. Lamo, Yngve; Wang, Xiaoliang; Mantz, Florian; Bech, Øyvind; Sandven, Anders; Rutle, Adrian: DPF workbench: a multi-level language workbench for MDE (2013) ioport
  10. Babiak, Tomáš; Řehák, Vojtěch; Strejček, Jan: Almost linear Büchi automata (2012)
  11. Barnat, Jiří; Bauch, Petr; Brim, Luboš; Češka, Milan: Designing fast LTL model checking algorithms for many-core GPUs (2012) ioport
  12. 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
  13. Barnat, Jiří; Brim, Luboš; Ročkai, Petr: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties (2012)
  14. Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jaco: Improved multi-core nested depth-first search (2012)
  15. Barnat, Jiří; Chaloupka, Jakub; van de Pol, Jaco: Distributed algorithms for SCC decomposition (2011)
  16. Bauch, Petr; Češka, Milan: CUDA accelerated LTL model checking -- revisited (2011)
  17. 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)
  18. Edelkamp, S.; Sulewski, D.; Barnat, J.; Brim, L.; Šimeček, P.: Flash memory efficient LTL model checking (2011)
  19. Edelkamp, Stefan; Sulewski, Damian: External memory breadth-first search with delayed duplicate detection on the GPU (2011) ioport
  20. Evangelista, Sami; Petrucci, Laure; Youcef, Samir: Parallel nested depth-first searches for LTL model checking (2011)

1 2 next

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