FormalMethods

From FedoraProject

(Difference between revisions)
Jump to: navigation, search
(Ongoing)
(Add reference to new page on suite; reorg)
Line 43: Line 43:
 
* Anyone have a preference?
 
* Anyone have a preference?
 
<!-- * Meeting minutes: [[SIGs/Robotics/Meetings| All]] - [[SIGs/Robotics/Meeting-20091015| Last (2009-10-15)]] -->
 
<!-- * Meeting minutes: [[SIGs/Robotics/Meetings| All]] - [[SIGs/Robotics/Meeting-20091015| Last (2009-10-15)]] -->
 +
 +
== Current Status ==
 +
 +
The [[Formal methods tool suite]] page identifies the tools that have been packaged, and categorizes them in normal English.
  
 
== Tasks ==
 
== Tasks ==
  
=== Recently Completed ===
+
=== Top to-dos ===
* Package "Why" updated to version 2.23 (needed for frama-C)
+
For packages that we'd like to see created, see the
* Package PVS; now packaged as pvs-sbcl
+
[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].
 +
 
 +
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)
  
 
=== Ongoing ===
 
=== Ongoing ===
Line 60: Line 70:
 
* Package Isabelle/HOL (Tim Colles?)
 
* Package Isabelle/HOL (Tim Colles?)
  
=== Top to-dos ===
+
=== Recently Completed ===
For packages that we'd like to see created, see the
+
* Package "Why" updated to version 2.23 (needed for frama-C)
[http://www.openproofs.org/wiki/Packaging_status Open Proofs packaging status] page.
+
* Package PVS; now packaged as pvs-sbcl
[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)
+
  
 
=== Yum group ===
 
=== Yum group ===
Line 74: Line 78:
 
We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness.  The current plan is to wait until frama-c is packaged, though if that takes too long, we can go ahead.
 
We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness.  The current plan is to wait until frama-c is packaged, though if that takes too long, we can go ahead.
  
 +
See the
 +
[[Formal methods tool suite]]
 +
page for a list of what would be in this group
 +
(along with their dependencies.
 
This would include at least the following packages (with their dependencies):
 
This would include at least the following packages (with their dependencies):
 
E,
 
E,

Revision as of 14:59, 20 January 2010

Contents

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 behaviors. 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:

Communication

The SIG will use the Fedora wiki, of course. Material that crosses beyond Fedora may also go into the open proofs site.

The mailing list to use is TBD:

Current Status

The Formal methods tool suite page identifies the tools that have been packaged, and categorizes them in normal English.

Tasks

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)

Ongoing

The following packages are our current focus and have someone working on them:

  • Package critically-needed pvs libraries, so "Why" can invoke them (jjames)
  • Update "Why" so it can invoke pvs-sbcl (jjames)
  • Package frama-c (adunn)
  • Package BLAST and its dependencies (picosat and csisat) (jjames; dwheeler reviewing)
  • Package ACL2 (jjames looking at)
  • Package Isabelle/HOL (Tim Colles?)

Recently Completed

  • Package "Why" updated to version 2.23 (needed for frama-C)
  • Package PVS; now packaged as pvs-sbcl

Yum group

We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of packagey goodness. The current plan is to wait until frama-c is packaged, though if that takes too long, we can go ahead.

See the Formal methods tool suite page for a list of what would be in this group (along with their dependencies. This would include at least the following packages (with their dependencies): E, alt-ergo, coq (coq-coqide, coq-doc, coq-emacs), cvc3, emacs-proofgeneral (emacs-common-proofgeneral, emacs-proofgeneral-el.noarch), xemacs-proofgeneral (xemacs-proofgeneral-el), frama-c {TODO}, minisat2, ppl (ppl-*), prover9 (prover9-apps, prover9-devel, prover9-doc), pvs-sbcl, sat4j, splint, stp (stp-devel), tex-zfuzz, why (why-coq, why-gwhy), zenon.

We might also add basic symbolic mathematics packages, since they can also be used for such purposes. These include: mathomatic, pari, sympy, wxMaxima / maxima.

Fedora Features

We could make this a proposed feature for the next release of Fedora; see the Fedora Features policy. Here is draft proposed text for a "Formal Methods" feature (previously named "provers").

Spin

In the longer term, we hope to create a Fedora Spin with these packages. That will need to wait until after the yum group is formed.