Here are a selection of research projects that I have worked on over the years.
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.
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.
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.
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.
FPRoCK is a software library for checking satisfiability of a set of mixed real and floating-point constraints.