Proposed new feature: Provers

David A. Wheeler dwheeler at dwheeler.com
Thu Aug 7 21:18:21 UTC 2008


I've developed info on a new feature of Fedora 10, aka "Provers":
 https://fedoraproject.org/wiki/Features/Provers
Basically, I and others have packaged some key
provers / solvers / formal methods tools.

Can anyone help us package some additional programs?
Some potential ones include:
* ACL2 (I have a start at this, it's written in Common Lisp)
* haRVey-FOL (depends on E and SPASS)
* BLAST, at http://mtc.epfl.ch/software-tools/blast/ (don't use the obsolete version at Berkeley)
* HOL 4
* Isabelle
* HOL Lite
* Gandalf
* NuSMV
* DiVinE
* KeY

You can find their descriptions and URLs here:
 http://www.dwheeler.com/essays/high-assurance-floss.html

--- David A. Wheeler 




More information about the fedora-devel-list mailing list