Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. Summary: Review Request: divine-mc - Multi-core model checking system for proving specifications https://bugzilla.redhat.com/show_bug.cgi?id=486757 Summary: Review Request: divine-mc - Multi-core model checking system for proving specifications Product: Fedora Version: rawhide Platform: All OS/Version: Linux Status: NEW Severity: medium Priority: medium Component: Package Review AssignedTo: nobody@xxxxxxxxxxxxxxxxx ReportedBy: dwheeler@xxxxxxxxxxxx QAContact: extras-qa@xxxxxxxxxxxxxxxxx CC: notting@xxxxxxxxxx, fedora-package-review@xxxxxxxxxx Estimated Hours: 0.0 Classification: Fedora Spec URL: http://www.dwheeler.com/divine-mc.spec SRPM URL: http://www.dwheeler.com/divine-mc-1.3-1.fc10.src.rpm Description: DiVinE Multi-Core (MC) is a parallel shared-memory enumerative model-checking tool for verification of concurrent systems. The tool can employ the full power of modern 64-bit multi-core architectures. It can be used to prove correctness of verification models as well as to detect early design errors. Any model-checking tool, such as DiViNe MC, accepts system requirements or design (called models) and a property (called specification) that the final system is expected to satisfy. The tool then outputs yes if the given model satisfies given specifications, and generates a counterexample otherwise. The counterexample details why the model doesn't satisfy the specification. DiViNe MC is based on automata-theoretic approach to linear temporal logics (LTL) model checking. The input language allows for specification of processes in terms of extended finite automata and the verified system is then obtained as an asynchronous parallel composition of these processes. In the current DiVinE Multi-Core release, input is provided in DVE format -- an industry-strength specification language, as used in original DiVinE, with plenty of diverse example models, ranging from simple toys to complex real-world models. An extensive model database is available at BEEM database. Moreover, DiVinE can read models specified in ProMeLa (as used in the SPIN tool), in addition to its native DVE format. However, the capabilities of the tool on ProMeLa models is currently limited by inability to produce counterexamples: you can only obtain a yes/no answer. -- Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email ------- You are receiving this mail because: ------- You are on the CC list for the bug. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review