[Bug 456398] New: Review Request: why - Why software verification platform

[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 report.




https://bugzilla.redhat.com/show_bug.cgi?id=456398

           Summary: Review Request: why - Why software verification platform
           Product: Fedora
           Version: rawhide
          Platform: All
        OS/Version: Linux
            Status: NEW
          Severity: medium
          Priority: medium
         Component: Package Review
        AssignedTo: nobody at fedoraproject.org
        ReportedBy: amdunn at gmail.com
         QAContact: extras-qa at fedoraproject.org
                CC: fedora-package-review at redhat.com,notting at redhat.com


Spec URL: http://www.duke.edu/~amd34/why/why.spec
SRPM URL: http://www.duke.edu/~amd34/why/why-2.13-1.fc9.src.rpm
Description: Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
(through the included tool "Caduceus"), Java (through the included
tool "Krakatoa"), and ML programs, but in theory is capable of
analysis of any program that is mapped onto its own internal
language. It uses a weakest precondition involving calculus to
generate potential theorems necessary for the proof of a program's
correctness. It translates these theorems into formats that can be
used by external proof assistants (without any extra work, Coq, PVS,
HOL Light, Mizar are supported - having one is recommended) and
automated theorem provers so that these results can be externally
proven, resulting in a proof of program correctness.

Current packaging notes:

- Builds on i386
- Builds in mock
- rpmlint silent
- Meets Fedora packaging criteria (to the best of my knowledge - went through the list)

-- 
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, or are watching someone who is.