< Features

(→Detailed Description) |
(Add sat4j) |
||

Line 36: | Line 36: | ||

Here are some of these kinds of tools, along with packages of programs | Here are some of these kinds of tools, along with packages of programs | ||

that perform them: | that perform them: | ||

− | * Automated Theorem Provers: These take mathematical facts and attempt to prove a goal, completely automatically. Packages: ''prover9'' | + | * Automated Theorem Provers: These take mathematical facts and attempt to prove a goal, completely automatically. Packages: ''prover9'', ''Zenon''. |

* Interactive Theorem Provers: These help humans take mathematical facts and attempt to prove a goal, in cases where the automated tools can't manage. Package: ''Coq'' | * Interactive Theorem Provers: These help humans take mathematical facts and attempt to prove a goal, in cases where the automated tools can't manage. Package: ''Coq'' | ||

* Program Provers: These take software code and work to prove claims about them, typically by breaking the code and claims into a large number of verification conditions (VCs) for the above to prove. Package: ''Why'' (for annotated C and Java) | * Program Provers: These take software code and work to prove claims about them, typically by breaking the code and claims into a large number of verification conditions (VCs) for the above to prove. Package: ''Why'' (for annotated C and Java) | ||

* Formal specification languages: These let people describe software or systems using a mathematically rigorous language, such as Z. Package: ''tex-zfuzz'' | * Formal specification languages: These let people describe software or systems using a mathematically rigorous language, such as Z. Package: ''tex-zfuzz'' | ||

− | * Boolean Satisfiability (SAT) solvers: These take boolean equations and solve for them; they are a basic building block for some implementations of the above. | + | * Boolean Satisfiability (SAT) solvers: These take boolean equations and solve for them; they are a basic building block for some implementations of the above. Packages: sat4j, ''[https://bugzilla.redhat.com/show_bug.cgi?id=453701 MiniSAT2]' |

Do ''not'' assume that you can just take a program prover on a big existing program and start | Do ''not'' assume that you can just take a program prover on a big existing program and start |

## Revision as of 20:35, 8 August 2008

## Contents

# Feature Name

Provers

## Summary

Add basic support for some key provers, solvers, and formal methods tools. These tools let you prove that some facts are true (given other facts) and/or model systems using mathematics. In some limited cases they can be used to greatly increase the reliability of software and hardware.

## Owner

- Name: David A. Wheeler

## Current status

- Targeted release: Fedora10
- Last updated: 2008-08-07
- Percentage of completion: 90% (MiniSAT packaged, but reviewer out of country)

## Detailed Description

No realistic software or hardware can be exhaustively tested; exhaustively testing a program that merely adds three 64-bit numbers would take more time than the Earth has existed. So for decades people have worked to develop tools that can apply mathematical techniques to prove that software and hardware (or a model of them) does or does not do something. These tools can also be used whenever it's important to prove something is true, or to solve for values given a large number of constraints.

Although these tools are still maturing, they are beginning to become useful in some limited circumstances. Now some key ones are packaged so developers on Fedora can begin to experiment with them.

Here are some of these kinds of tools, along with packages of programs that perform them:

- Automated Theorem Provers: These take mathematical facts and attempt to prove a goal, completely automatically. Packages:
*prover9*,*Zenon*. - Interactive Theorem Provers: These help humans take mathematical facts and attempt to prove a goal, in cases where the automated tools can't manage. Package:
*Coq* - Program Provers: These take software code and work to prove claims about them, typically by breaking the code and claims into a large number of verification conditions (VCs) for the above to prove. Package:
*Why*(for annotated C and Java) - Formal specification languages: These let people describe software or systems using a mathematically rigorous language, such as Z. Package:
*tex-zfuzz* - Boolean Satisfiability (SAT) solvers: These take boolean equations and solve for them; they are a basic building block for some implementations of the above. Packages: sat4j,
*MiniSAT2'*

Do *not* assume that you can just take a program prover on a big existing program and start
using it effectively; program prover tools are just *starting* to become mature.
All such tools have limitations, scale can be a problem, and it's typically more effective
to develop the proofs simultaneously with the program.
Nevertheless, for those who are interested in the technology, have small-scale problems
where they can be applied, or who wish to help it mature,
these are a great place to start.

SAT solvers *have* been used in a variety of places.
Another distribution is using a SAT solver to speed up RPM dependency analysis.

For more information, and a list of FLOSS tools, see Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods / Software Verification.

## Benefit to Fedora

This enables developers to start using these kinds of programs in a variety of circumstances.

## Scope

Developers have had to package a number of programs, most of which have not been packaged before. In some cases, we've had to address integration problems (e.g., Zenon changed its input format, but the Why developers didn't know that). It has no effect on those who don't wish to use these tools.

We had hoped to add CVC3 to Fedora, but the current CVC3 license includes some highly problematic clauses, so CVC3 will currently not be included. There is some hope of also adding PVS and Alt-Ergo before the release of Fedora 10, but they are not required to have a reasonable initial set of provers and related tools available in Fedora 10.

It is expected that future versions of Fedora will build on this, adding more tools to handle different circumstances.

## Test Plan

No special hardware or system preparation is required; simply install the packages listed above. Many of the toolsuites include some checking. In addition, the "Why" suite can use many other tools; we have used its "binary-search.c" example with gwhy to test integration with Zenon and Coq.

## User Experience

Target users will notice that they can easily install these tools.

## Dependencies

There are no special dependencies.

## Contingency Plan

None necessary, revert any undesirable packages.

## Documentation

Documentation on these tools is notoriously bad; some tool developers (including MiniSAT and Zenon) don't provide any documentation at all. We have written some brief documentation in some cases, to help people get started. We expect this to improve in future releases; it will also be easier to get people to write documentation once the programs themselves are easier to install.

## Release Notes

No special release notes.