DiVinE: Parallel Distributed Model Checker
Jǐŕı Barnat, Luboš Brim, Milan Češka, Petr Ročkai · 2010
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. While the main focus of the tool is on high-performance explicit state model checking, an emphasis is also put on ease of deployment and usage. Additionally, the component architecture and publicly available source code of DiVinE allow for its usage as a platform for research on parallel and distributed-memory model checking techniques.