DiVinE Multi-Core

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE Multi-Core. 2007.

Basic information

• Original name: DiVinE Multi-Core
• Name in Czech: DiVinE Multi-Core
• Authors: BARNAT, Jiří (203 Czech Republic), Luboš BRIM (203 Czech Republic, guarantor) and Petr ROČKAI (203 Czech Republic).
• Edition: 2007.

Other information

• Original language: English
• Type of outcome: Software
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/07:00019614
• Organization unit: Faculty of Informatics
• Keywords in English: parallel verification; multi-core architecture; model-checking
• Technical parameters: Paralelní verifikační nástroj pro ověřování modelů LTL vlastností.
• Tags: Model-Checking, multi-core architecture, parallel verification
• Tags: International impact

Abstract

Based on proven DiVinE LTL model checking system, DiVinE Multi-Core brings parallel verification to contemporary high-powered multi-core architectures. DiVinE Multi-Core exploits full power of modern x86 hardware and reduces unnecessary delays in workflow. Employing state-of-the-art parallel liveness checking algorithm, DiVinE Multi-Core offers unmatched scalability on shared memory platforms in the range of 2- to 16-core machines. Moreover, the tool supports 64-bit platforms out of the box, allowing it to leverage all the memory available in contemporary systems (and systems of the upcoming years).

Abstract (in Czech)

DiVinE-MC je paralelní nástroj pro verifikaci LTL vlastností. Nástroj pouzívá algoritmy pro práci ve sdílené pameti na více-jadrových systémech.

Links

• GA201/06/1338, research and development project: Name: Automatizovaná verifikace softwaru

Investor: Czech Science Foundation, Automated software verification

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems