DiVinE 2.0: High-Performance Model Checking

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BARNAT Jiří BRIM Luboš ROČKAI Petr
Year of publication	2009
Type	Article in Proceedings
Conference	International Workshop on High Performance Computational Systems Biology
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	LTL Model Checking
Description	We present a tool for parallel enumerative LTL model-checking and reachability analysis. The tool brings model checking to high-powered multi-core systems, as well as high-performance clusters. Boasting pluggable modelling language framework, it is possible to leverage the available parallel algorithms for multiple problem domains, by using suitable input language.
Related projects:	Techniques for automatic verification and validation of software nad hardware systems Highly Parallel and Distributed Computing Systems Verification and Analysis of Large-Scale Computer Systems Automated formal verification using modern hardware