Abstract
We present a tool for cluster-based LTL model-checking and reachability analysis. The tool incorporates several novel distributed-memory algorithms and provides a unique interface to use them. We describe the basic structure of the tool, discuss the main architecture decisions made, and briefly explain how the tool can be used.
This work has been partially supported by the Grant Agency of Czech Republic grant No. 201/06/1338 and the Academy of Sciences grant No. 1ET408050503.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barnat, J., Brim, L., Černá, I.: Distributed Analysis of Large Systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111. Springer, Heidelberg (2006)
Barnat, J., Forejt, V., Leucker, M., Weber, M.: DivSPIN – A SPIN compatible distributed model checker. In: Proc. 4th International Workshop on Parallel and Distributed Methods in verification, pp. 95–100 (2005)
Behrmann, G., Hune, T.S., Vaandrager, F.W.: Distributed timed model checking — how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)
Bollig, B., Leucker, M., Weber, M.: Parallel model checking for the alternation free μ-calculus. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 543–558. Springer, Heidelberg (2001)
DiVinE project web page: http://anna.fi.muni.cz/divine/
Garavel, H., Mateescu, R., Smarandache, I.M.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 200–216. Springer, Heidelberg (2001)
Holmen, F., Leucker, M., Lindstrom, M.: Uppdmc: A distributed model checker for fragments of the mu-calculus. Electronic Notes in Theoretical Computer Science 128(3), 91–105 (2005)
Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P. (2006). DiVinE – A Tool for Distributed Verification. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_26
Download citation
DOI: https://doi.org/10.1007/11817963_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)