DiVinE – A Tool for Distributed Verification
作者： Jiří Barnat , Luboš Brim , Ivana Černá , Pavel Moravec , Petr Ročkai
DOI: 10.1007/11817963_26
关键词:
摘要: We present a tool for cluster-based LTL model-checking and reachability analysis. The incorporates several novel distributed-memory algorithms provides unique interface to use them. describe the basic structure of tool, discuss main architecture decisions made, briefly explain how can be used.
springer.com
springerlink.com参考文章(8)
Vojtěch Forejt, Martin Leucker, Jiří Barnat, Michael Weber, DivSPIN - A SPIN compatible distributed model checker TU Munchen. pp. 95- 100 ,(2005)
Gerd Behrmann, Thomas Hune, Frits Vaandrager, Distributing Timed Model Checking - How the Search Order Matters computer aided verification. pp. 216- 231 ,(2000) , 10.1007/10722167_19
Flavio Lerda, Riccardo Sisto, Distributed-Memory Model Checking with SPIN international workshop on model checking software. ,vol. 1680, pp. 22- 39 ,(1999) , 10.1007/3-540-48234-2_3
Hubert Garavel, Radu Mateescu, Irina Smarandache, Parallel state space construction for model-checking international workshop on model checking software. pp. 217- 234 ,(2001) , 10.5555/380921.380941
Jiří Barnat, Luboš Brim, Ivana Černá, Cluster-Based LTL model checking of large systems formal methods. pp. 259- 279 ,(2005) , 10.1007/11804192_13
Fredrik Holmén, Martin Leucker, Marcus Lindström, UppDMC: A Distributed Model Checker for Fragments of the μ-Calculus Electronic Notes in Theoretical Computer Science. ,vol. 128, pp. 91- 105 ,(2005) , 10.1016/J.ENTCS.2004.10.021
Luboš Brim, Ivana Černá, Jiří Barnat, Distributed Analysis of Large Systems CWI Amsterdam. pp. 31- 35 ,(2005)
Gerhard Schellhorn, Wolfgang Reif, Martin Leucker, Parallel Model Checking for the Alternation-Free Mu-Calculus FM-TOOLS 2000, The 4th Workshop on Tools for System Design and Verification. ,(2000)