Projects

VSCode-PRECiSA

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 …

Paolo Masci
•
Read more

ReFlow

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. …

Laura Titolo
•
Read more

PRECiSA

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 …

Laura Titolo
•
Read more

FRET Proof Framework

Rigorous PVS formalization of the Fretish structured natural language. It includes a new denotational semantics and a proof of semantic equivalence between Fretish specifications …

Laura Titolo
•
Read more

FPRoCK

FPRoCK is a software library for checking satisfiability of a set of mixed real and floating-point constraints.

Rocco Salvia
•
Read more

CPR*

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 …

Aaron Dutle
•
Read more