FormalMethods

From FedoraProject

(Difference between revisions)
Jump to: navigation, search
(Ongoing)
(General clean-up. Removed outdated references to efforts that have since been completed (e.g. packaging Frama-C).)
 
(10 intermediate revisions by 6 users not shown)
Line 2: Line 2:
  
 
== What are Formal Methods? ==
 
== What are Formal Methods? ==
"Formal methods" are techniques that use mathematics
+
"Formal Methods" are techniques that apply [http://en.wikipedia.org/wiki/Formal_proof Formal Proof] techniques from Mathematics to prove that models of software, hardware, or systems will or will not have certain properties, or exhibit certain behaviors. Many Free/Libre/Open Source Software (FLOSS) tools for formal methods are becoming available, including automated theorem provers and model-checkers, but the tools can be difficult to install and apply.
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 ==
 
== Goal and Scope ==
The goal of the Formal Methods SIG is to make it easy to
+
The goal of the Formal Methods SIG is to make it easy to install formal methods tools in Fedora, to ease the process of learning how to apply them, to encourage the development of "open proofs" (where an implementation, proofs, and the required tools are all FLOSS), and to provide feedback to tool developers so that the tools in Fedora can become more powerful, more scaleable, and easier to use together.
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 ==
 
== Mission and Plan ==
Line 33: Line 22:
 
* [[User:mnagy|Martin Nagy]]
 
* [[User:mnagy|Martin Nagy]]
 
* [[User:agoode|Adam Goode]]
 
* [[User:agoode|Adam Goode]]
 +
* [[User:ifkaluva|Nikos Arechiga]]
 +
* [[User:jcp|John C. Peterson]]
 +
* [[User:andrewj|Andrew V. Jones]]
 +
* [[User:borgan|Brock Organ]]
 
* '''Please add your name here!'''
 
* '''Please add your name here!'''
  
 
== Communication ==
 
== Communication ==
The SIG will use the Fedora wiki, of course. Material that crosses beyond Fedora may also go into the [http://www.openproofs.org open proofs site].
+
The SIG will naturally use the Fedora Wiki. Material of a more general nature that crosses beyond Fedora to other Linux distributions may also go on the [http://www.openproofs.org Open Proofs] site. The mailing list to use is TBD:
 
+
The mailing list to use is TBD:
+
 
* We could create a [https://www.redhat.com/mailman/listinfo/fedora-formalmethods-list Fedora Formal Methods List].
 
* We could create a [https://www.redhat.com/mailman/listinfo/fedora-formalmethods-list Fedora Formal Methods List].
* Alternatively, we could just use the [http://lists.openproofs.org/mailman/listinfo/openproofs existing open proofs mailing list]. Two advantages of using this: (1) it already exists, and (2) it will help us re-use and coordinate with other distros.
+
* Alternatively, we could just use the existing [http://lists.openproofs.org/mailman/listinfo/openproofs Open Proofs mailing list]. Two advantages of using this: (1) it already exists, and (2) it will help us re-use and coordinate with other distros.
 
* 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)]] -->
 +
 +
== Currently Available Packages ==
 +
The [[Formal_methods_tool_suite|Formal Methods Tool Suite]] page identifies the tools that have already been packaged for Fedora. The list is organized in a way that (hopefully) makes what they can do, and how they do it easier to understand.
  
 
== Tasks ==
 
== Tasks ==
  
=== Recently Completed ===
+
=== Active Packaging Efforts ===
* Package "Why" updated to version 2.23 (needed for frama-C)
+
The following packages are our current focus and have someone actively working on them:
* Package PVS; now packaged as pvs-sbcl
+
* [http://www.cs.utexas.edu/users/moore/acl2/ ACL2] (Jerry James)
 +
* [http://mtc.epfl.ch/software-tools/blast/ BLAST] (Jerry James, David Wheeler, see [https://bugzilla.redhat.com/show_bug.cgi?id=555162 ticket 555162])
 +
* [http://www.cs.unm.edu/~mccune/eqp/ EQP] (John Peterson, see [https://bugzilla.redhat.com/show_bug.cgi?id=769958  ticket 769958])
 +
* [http://isabelle.in.tum.de/ Isabelle / HOL] (Tim Colles?)
  
=== Ongoing ===
+
=== Package Want List ===
The following packages are our current focus and have someone working on them:
+
Here are some upstream projects that we would like to see packaged. Jerry James has draft packages for some of these on his [http://jjames.fedorapeople.org/ Fedora People] page. For some more ideas, see the [http://www.openproofs.org/wiki/Packaging_status Packaging Status] page at the [http://www.openproofs.org/wiki/Main_Page Open Proofs] site.
 +
* [http://apron.cri.ensmp.fr/library/ APRON] (a draft is available)
 +
* [http://czt.sourceforge.net/index.html Community Z Tools] (Anyone?)
 +
* [http://divine.fi.muni.cz/ DiVinE] (Anyone?)
 +
* [http://maude.cs.uiuc.edu/ Maude] (Anyone?)
 +
* [http://www.spass-prover.org/ SPASS] (Anyone?)
  
* Package critically-needed pvs libraries, so "Why" can invoke them (jjames)
+
=== Yum Group ===
* Update "Why" so it can invoke pvs-sbcl (jjames)
+
We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of package goodness.  The current plan is to wait until Frama-C is packaged. However, if that takes too long, we might proceed sooner than that. See the [[Formal_methods_tool_suite|Formal Methods Tool Suite]] page for a list of the packages that would be in this group (along with their dependencies).
* Package frama-c (adunn)
+
* [https://bugzilla.redhat.com/show_bug.cgi?id=555162 Package BLAST and its dependencies] (jjames)
+
* Package ACL2 (jjames looking at)
+
* Package Isabelle/HOL (Tim Colles?)
+
 
+
=== Top to-dos ===
+
For packages that we'd like to see created, see the
+
[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)
+
 
+
=== 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 other page.  Here's the old list:
 
This would include at least the following packages (with their dependencies):
 
This would include at least the following packages (with their dependencies):
 
E,
 
E,
Line 91: Line 76:
 
why (why-coq, why-gwhy),
 
why (why-coq, why-gwhy),
 
zenon.
 
zenon.
 
+
-->
We ''might'' also add basic symbolic mathematics packages, since they can also be used for such purposes. These include:
+
We ''might'' also include some symbolic mathematics packages, since they can also be used for such purposes. These include: mathomatic, maxima, wxMaxima, pari, sympy.
mathomatic, pari, sympy, wxMaxima / maxima.
+
  
 
=== Fedora Features ===
 
=== Fedora Features ===
  
 
We could make this a proposed feature for the next release of Fedora; see the
 
We could make this a proposed feature for the next release of Fedora; see the
[https://fedoraproject.org/wiki/Features/Policy Fedora Features policy].
+
[https://fedoraproject.org/wiki/Features/Policy Fedora Features policy]. Here is a
[https://fedoraproject.org/wiki/Features/Formal_Methods Here is draft proposed text for a "Formal Methods" feature (previously named "provers")].
+
[https://fedoraproject.org/wiki/Features/Formal_Methods draft proposed text] for a "Formal Methods" feature (previously named "provers").
 +
 
 +
=== Formal Methods Spin ===
  
=== Spin ===
+
In the longer term, we hope to create a Fedora Spin with these packages. This will need to wait until after the yum group has been created. The [[Haskell Spin]] kickstart file might be a useful place to start.
  
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.
+
== Recently Completed Tasks ==
 +
* Approved package Frama-C (frama-c)
 +
* Package "Why" updated to version 2.23 (needed for Frama-C)
 +
* Approved package PVS (pvs-sbcl)
 +
* Approved packages csisat, picosat (needed for BLAST)
 +
* Created the [[Formal_methods_tool_suite|Formal Methods Tool Suite]] page
  
 
[[Category:SIGs]]
 
[[Category:SIGs]]
 
[[Category:Packaging SIGs]]
 
[[Category:Packaging SIGs]]
 +
[[Category:Fedora special-interest groups|Formal Methods]]

Latest revision as of 06:22, 29 October 2012

Contents

[edit] Fedora Formal Methods Special Interest Group (SIG)

[edit] What are Formal Methods?

"Formal Methods" are techniques that apply Formal Proof techniques from Mathematics to prove that models of software, hardware, or systems will or will not have certain properties, or exhibit certain behaviors. Many Free/Libre/Open Source Software (FLOSS) tools for formal methods are becoming available, including automated theorem provers and model-checkers, but the tools can be difficult to install and apply.

[edit] Goal and Scope

The goal of the Formal Methods SIG is to make it easy to install formal methods tools in Fedora, to ease the process of learning how to apply them, to encourage the development of "open proofs" (where an implementation, proofs, and the required tools are all FLOSS), and to provide feedback to tool developers so that the tools in Fedora can become more powerful, more scaleable, and easier to use together.

[edit] Mission and Plan

For more details, see the Mission Statement and Plan for the Formal Methods Fedora SIG.

[edit] Members

Co-Leads:

Others:

[edit] Communication

The SIG will naturally use the Fedora Wiki. Material of a more general nature that crosses beyond Fedora to other Linux distributions may also go on the Open Proofs site. The mailing list to use is TBD:

  • We could create a Fedora Formal Methods List.
  • Alternatively, we could just use the existing Open Proofs mailing list. Two advantages of using this: (1) it already exists, and (2) it will help us re-use and coordinate with other distros.
  • Anyone have a preference?

[edit] Currently Available Packages

The Formal Methods Tool Suite page identifies the tools that have already been packaged for Fedora. The list is organized in a way that (hopefully) makes what they can do, and how they do it easier to understand.

[edit] Tasks

[edit] Active Packaging Efforts

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

[edit] Package Want List

Here are some upstream projects that we would like to see packaged. Jerry James has draft packages for some of these on his Fedora People page. For some more ideas, see the Packaging Status page at the Open Proofs site.

[edit] Yum Group

We intend to create a "formal methods" yum group soon, so that 'yum groupinstall "Formal methods"' will get you lots of package goodness. The current plan is to wait until Frama-C is packaged. However, if that takes too long, we might proceed sooner than that. See the Formal Methods Tool Suite page for a list of the packages that would be in this group (along with their dependencies).

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

[edit] Fedora Features

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

[edit] Formal Methods Spin

In the longer term, we hope to create a Fedora Spin with these packages. This will need to wait until after the yum group has been created. The Haskell Spin kickstart file might be a useful place to start.

[edit] Recently Completed Tasks

  • Approved package Frama-C (frama-c)
  • Package "Why" updated to version 2.23 (needed for Frama-C)
  • Approved package PVS (pvs-sbcl)
  • Approved packages csisat, picosat (needed for BLAST)
  • Created the Formal Methods Tool Suite page