No edit summary |
(→Tasks) |
||
| Line 37: | Line 37: | ||
== Tasks == | == Tasks == | ||
The following packages are our current focus: | === Ongoing === | ||
The following packages are our current focus and have someone working on them: | |||
* Package update for "Why" so 2.23 is in Fedora repository (adunn) | * Package update for "Why" so 2.23 is in Fedora repository (adunn) | ||
* Package critically-needed pvs libraries, so "Why" can invoke them (jjames) | * Package critically-needed pvs libraries, so "Why" can invoke them (jjames) | ||
* Package frama-c (adunn?) | * Package frama-c (adunn?) | ||
* Package ACL2 (jjames looking at) | * Package ACL2 (jjames looking at) | ||
=== Top to-dos === | |||
For packages that we'd like to see created, see the | For packages that we'd like to see created, see the | ||
[http://www.openproofs.org/wiki/Packaging_status Open Proofs packaging status] page. | [http://www.openproofs.org/wiki/Packaging_status Open Proofs packaging status] page. | ||
[http://jjames.fedorapeople.org/ Jerry James has draft packages for some of these]. | [http://jjames.fedorapeople.org/ Jerry James has draft packages for some of these]. | ||
Of those, in particular it'd be great to see: | |||
* Package APRON (a draft is available) | |||
* Package Isabelle/HOL | |||
* Package DiVinE-MC (a draft is available) | |||
We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness. In the longer term, we hope to create a Fedora Spin with these packages. | We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness. In the longer term, we hope to create a Fedora Spin with these packages. | ||
[[Category:SIGs]] | [[Category:SIGs]] | ||
Revision as of 23:03, 11 January 2010
Fedora Formal Methods Special Interest Group (SIG)
What are Formal Methods?
"Formal methods" are techniques that use mathematics to prove that models of software, hardware, or systems will or will not have certain behavior. To be practical, they must be automated using tools. Free/Libre/Open Source Software (FLOSS) formal methods tools are now available, including automated theorem provers and model-checkers, but the tools can be difficult to install and apply.
Goal and Scope
The goal of the Formal Methods SIG is to make it easy to install formal methods tools in Fedora, ease learning how to apply them, encourage the development of "open proofs" (where an implementation, proofs, and required tools are all FLOSS), and to provide feedback to toolmakers so that the tools in Fedora can become more powerful, more scaleable, and easier to use together.
Mission and Plan
For more details, see the Mission Statement and Plan for the Formal Methods Fedora SIG.
Members
Co-Leads:
Others:
- Alan Dunn
- Klaus Grue
- Please add your name here!
Communication
- Mailing list: TBD. We may create a Fedora Formal Methods List. Alternatively, we may just use the existing open proofs mailing list... anyone have a preference?
Tasks
Ongoing
The following packages are our current focus and have someone working on them:
- Package update for "Why" so 2.23 is in Fedora repository (adunn)
- Package critically-needed pvs libraries, so "Why" can invoke them (jjames)
- Package frama-c (adunn?)
- Package ACL2 (jjames looking at)
Top to-dos
For packages that we'd like to see created, see the Open Proofs packaging status page. Jerry James has draft packages for some of these.
Of those, in particular it'd be great to see:
- Package APRON (a draft is available)
- Package Isabelle/HOL
- Package DiVinE-MC (a draft is available)
We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness. In the longer term, we hope to create a Fedora Spin with these packages.