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

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

1 2 3 next

  1. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  2. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  3. Chini, Peter; Kolberg, Jonathan; Krebs, Andreas; Meyer, Roland; Saivasan, Prakash: On the complexity of bounded context switching (2017)
  4. Barnat, Jiří; Bauch, Petr; Beneš, Nikola; Brim, Luboš; Beran, Jan; Kratochvíla, Tomáš: Analysing sanity of requirements for avionics systems (2016)
  5. Bérard, Béatrice; Lafourcade, Pascal; Millet, Laure; Potop-Butucaru, Maria; Thierry-Mieg, Yann; Tixeuil, Sébastien: Formal verification of mobile robot protocols (2016)
  6. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  7. Barnat, Jiří: Quo vadis explicit-state model checking (2015)
  8. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  9. Wang, Bing; Deng, Bo; Xing, Fei; Wang, Dongxia; Yao, Yiping: Partitioned event graph: formalizing LP-based modelling of parallel discrete-event simulation (2015)
  10. Brim, L.; Dluhoš, P.; Šafránek, D.; Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator (2014)
  11. Alechina, Natasha; Bassiliades, Nick; Dastani, Mehdi; De Vos, Marina; Logan, Brian; Mera, Sergio; Morris-Martin, Andreasa; Schapachnik, Fernando: Computational models for normative multi-agent systems (2013)
  12. Barnat, Jiří; Brim, Luboš; Havel, Vojtěch; Havlíček, Jan; Kriho, Jan; Lenčo, Milan; Ročkai, Petr; Štill, Vladimír; Weiser, Jiří: Divine 3.0 -- an explicit-state model checker for multithreaded C (&) C++ programs (2013) ioport
  13. Brim, Luboš; Češka, Milan; Šafránek, David: Model checking of biological systems (2013)
  14. 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)
  15. Evangelista, Sami; Kristensen, Lars Michael: Dynamic state space partitioning for external memory state space exploration (2013) ioport
  16. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  17. Lamo, Yngve; Wang, Xiaoliang; Mantz, Florian; Bech, Øyvind; Sandven, Anders; Rutle, Adrian: DPF workbench: a multi-level language workbench for MDE (2013) ioport
  18. Babiak, Tomáš; Řehák, Vojtěch; Strejček, Jan: Almost linear Büchi automata (2012)
  19. Barnat, Jiří; Bauch, Petr; Brim, Luboš; Češka, Milan: Designing fast LTL model checking algorithms for many-core GPUs (2012) ioport
  20. 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

1 2 3 next

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