VSCode-PRECiSA is a toolkit that integrates the PRECiSA floating-point round-off error analyzer into Visual Studio Code. The toolkit provides an intuitive graphical user interface and offers different analysis views for experimenting and reasoning about how floating-point errors affect the computed result of a program.
Sep 9, 2024
ReFlow extracts floating-point C code from a PVS real numbers specification. The code is annotated with ACSL pre- and post-conditions that bound the accumulated round-off error. ReFlow can also instrument the C code to detect when the floating-point control flow diverges with respect to the ideal real numbers' one.
Sep 9, 2024
PRECiSA is a static analyzer that estimates the accumulated round-off error of floating-point programs. It automatically generates PVS proof certificates that guarantee the correctness of the error estimations with respect to the floating-point IEEE-754 standard. It is designed to support a compositional static analysis of the program and it support a large variety of operators and program constructs.
Sep 9, 2024
Rigorous PVS formalization of the Fretish structured natural language. It includes a new denotational semantics and a proof of semantic equivalence between Fretish specifications and their temporal logic counterparts computed by Fret.
Jan 17, 2022
FPRoCK is a software library for checking satisfiability of a set of mixed real and floating-point constraints.
May 7, 2019
CPR* is a formally verified C implementation of the Compact Position Reporting (CPR) algorithm, a key component of the ADS-B standard responsible for encoding and decoding aircraft positions.
Jun 23, 2018