[Bug 486757] New: Review Request: divine-mc - Multi-core model checking system for proving specifications

[bugzilla at redhat.com]

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 at fedoraproject.org
        ReportedBy: dwheeler at dwheeler.com
         QAContact: extras-qa at fedoraproject.org
                CC: notting at redhat.com, fedora-package-review at redhat.com
   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.