| CARVIEW |
PropaFP: Auto-active verification of floating-point programs
Modules
[Index] [Quick Jump]
- PropaFP
Downloads
- PropaFP-0.1.2.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
| Versions [RSS] | 0.1.0.0, 0.1.1.0, 0.1.2.0 |
|---|---|
| Change log | ChangeLog.md |
| Dependencies | aern2-mfun (>=0.2.9 && <0.3), aern2-mp (>=0.2.9.1 && <0.3), base (>=4.7 && <5), 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 |
| Uploaded | by JunaidRasheed at 2023-03-12T23:28:48Z |
| 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 |
| Distributions | |
| 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 | 290 total (14 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 2023-03-12 [all 2 reports] |
Readme for PropaFP-0.1.2.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 (arXiv version).
Below is a diagram summarising the integration with PropaFP and SPARK.
Requirements
All PropaFP executables require the FPTaylor v0.9.4 executable in $PATH.
The 'propafp-run-$prover' executables require the $prover to be installed (but not necessarily in $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 state where the PropaFP executables have been placed.
Supported Provers
Currently, PropaFP supports:
- dReal4 (Tested on v4.21.06.2)
- LPPaver (Tested on v0.1.0.0)
- MetiTarski (Tested on v2.4)
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 $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, pass the -c option.
PropaFP with GNAT Studio
For instructions to use with GNAT Studio 2022, see sparkFiles/INSTRUCTIONS.md