PropaFP: Auto-active verification of floating-point programs

[ formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers ] [ Propose Tags ]

Please see the README on GitHub at https://github.com/rasheedja/PropaFP#readme


[Skip to Readme]

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.1.1.0
Change log ChangeLog.md
Dependencies aern2-mfun (>=0.2.9 && <0.3), aern2-mp (>=0.2.9.1 && <0.3), base (>=4.15.1.0 && <4.16), binary (>=0.8.8.0 && <0.9), bytestring (>=0.10.12.1 && <0.11), collect-errors (>=0.1.5 && <0.2), containers (>=0.6.4.1 && <0.7), directory (>=1.3.6.2 && <1.4), extra (>=1.7.10 && <1.8), ghc (>=9.0.2 && <9.1), mixed-types-num (>=0.5.10 && <0.6), optparse-applicative (>=0.16.1.0 && <0.17), process (>=1.6.13.2 && <1.7), PropaFP, QuickCheck (>=2.14.2 && <2.15), regex-tdfa (>=1.3.1.2 && <1.4), scientific (>=0.3.7.0 && <0.4), temporary (>=1.3 && <1.4) [details]
License MPL-2.0
Copyright MPL-2.0
Author Junaid Rasheed
Maintainer jrasheed178@gmail.com
Revised Revision 1 made by JunaidRasheed at 2022-10-13T12:44:44Z
Category Math, Maths, Mathematics, Formal methods, Theorem Provers
Home page https://github.com/rasheedja/PropaFP#readme
Bug tracker https://github.com/rasheedja/PropaFP/issues
Source repo head: git clone https://github.com/rasheedja/PropaFP
Uploaded by JunaidRasheed at 2022-10-13T11:05:32Z
Distributions NixOS:0.1.1.0
Reverse Dependencies 1 direct, 0 indirect [details]
Executables propafp-translate-metitarski, propafp-translate-dreal, propafp-run-metitarski, propafp-run-lppaver, propafp-run-dreal, propafp-prettify
Downloads 53 total (7 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user [build log]
All reported builds failed as of 2022-10-13 [all 1 reports]

Readme for PropaFP-0.1.1.0

[back to package description]

PropaFP

PropaFP is a tool used for auto-active verification of Floating-Point programs. PropaFP can be used for the verification of SPARK/Ada floating-point programs and is integrated with GNAT Studio 2022.

PropaFP can take some Verification Condition (VC), and if PropaFP understands the VC, simplify it, derive bounds for variables, and safely eliminate floating-point operations using over-approximations on rounding errors. A more detailed description of PropaFP can be found in this paper.

Below is a diagram summarising the integration with PropaFP and SPARK.

SPARK + PropaFP

Requirements

All PropaFP executables require the FPTaylor v0.9.3 executable in your $PATH.

The 'propafp-run-$prover' executables require you to have $prover installed (but not necessarily in your $PATH).

To build PropaFP, we recommend Stack. We have built PropaFP with Stack version 2.7.5.

Installation

  • Download/Clone this repository
  • cd into the repo
  • Run stack build

Stack will then build the project and tell you where the PropaFP executables have been placed.

Supported Provers

Currently, PropaFP supports:

Usage

PropaFP can work as a standalone program or with GNAT Studio 2022.

PropaFP as a Standalone Program

To produce some input for PropaFP, see the Reference.

Translator Executables

PropaFP contains 'translator' executables, which takes some input file, transforms the VC as described above, and produces another input file for the target prover. The current 'translator' executables are:

  • propafp-translate-dreal -f [smtFileContainingVC.smt2] -t [fileToWrite.smt2]
  • propafp-translate-metitarski -f [smtFileContainingVC.smt2] -t [fileToWrite.smt2]

The propafp-translate-dreal executable can also be used for LPPaver. If PropaFP does not understand the VC, it writes an empty file.

Runner Executables

'Runner' executables take some input file, transform the VC as described above, and calls the prover on the transformed VC. 'Runner' executables require the prover for each executable to be in your $PATH. The current 'runner' executables are:

  • propafp-run-dreal -f [smtFileContainingVC.smt2] -p [pathToDReal]
  • propafp-run-lppaver -f [smtFileContainingVC.smt2] -p [pathToLPPaver]
  • propafp-run-metitarski -f [smtFileContainingVC.smt2] -p [pathToMetiTarski]

To run LPPaver in a mode specialised to find counter-examples, you can pass the -c option.

PropaFP with GNAT Studio

For instructions to use with GNAT Studio 2022, see sparkFiles/INSTRUCTIONS.md

Guided Example

A guided example of using PropaFP with GNAT Studio.