Here is a collection of RPMs that I have put together. They are here for me to test. Those that seem satisfactory will eventually be pushed into either Fedora or RPM Fusion, depending on licensing issues. If an RPM disappears from this page, then I have either found it unsatisfactory or migrated it into one of those two collections.

**Note:** Due to space problems, I am not able to post
binary RPMs on this web page. Furthermore, some of the programs listed
here are distributed under non-free licenses, so I cannot provide the
sources either. Hence, all you get is either src or norsrc RPMs.

These packages are freely distributable. I provide source RPMs for each.

- buddy: BDD library.
- cal: BDD library.
- cmusphinx4: speech recognition.
- CrocoPat: a relational programming tool.
- dedukti: universal proof checker.
- fest-maven-setup: FEST parent pom.
- fest-test: Common testing infrastructure for FEST.
- fest-util: FEST utilities.
- java-colors: color chooser for Java.
- JHotDraw: a Java GUI framework for technical and structured graphics.
- jreality: 3D mathematical visualization in Java.
- jtem-beans: auto-generate a GUI to inspect JavaBeans.
- jtem-jrworkspace: tool to build UIs for complex modular applications.
- jtem-jterm: Java terminal window.
- jtem-mfc: Mathematical Foundation Classes for Java.
- jtem-numericalMethods: a Java library that computes numerical solutions to algebra, calculus, and geometry problems.
- libpoly: C library for manipulating polynomials.
- LiDIA: a library for computational number theory.
- netutil: Open Sound Control (OSC) for Java.
- opendial: a generic Java-based toolkit for building dialog systems.
- SInE: Sumo Inference Engine, a metaprover targeted on large theories, especially on SUMO.
- smrj: Simple multicast remote Java.
- snark: SRI's New Automated Reasoning Kit.
- spass: SPASS, an automated theorem prover for first-order logic with equality.
- Spin: a model checker.
- sunflow: Java rendering system for photo-realistic image synthesis.

These packages are supposedly free software or open source, but include license terms that are incompatible with the Fedora distribution.

- blast: Berkeley Lazy Abstraction Software verification Tool.
- cmuclmtk: a language model trainer for the CMU Sphinx decoders.

These packages have restrictive licenses. I do not provide the sources. You have to download those yourself after signifying your agreement with the license terms. All I provide is a nosrc RPM.

- pvs: Prototype Specification and Verification System (Allegro Common Lisp version).
- yices: an efficient SMT solver.
- zChaff: a Boolean Satisfiability solver.

These packages are clearly intended to be free, given statements by their authors. However, the authors have failed to provide a clear license, making them unacceptable to repositories with lawyers.

- nasalib: NASA Langley collection of PVS theories.

Last modified: Thu Dec 8 20:49:55 MST 2016 by Jerry James