DiVinE 2.0: High-Performance Model Checking

• 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
• 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