I am PC-(co)chair of the 13th NASA Formal Methods Symposium (NFM 2021) together with Aaron Dutle and Mariano Moscato.

I am a member of the program committee of the 13th International Workshop on Numerical Software Verification (NSV 2020).

I am a member of the program committee of the 12th NASA Formal Methods Symposium (NFM 2020).



Research Scientist

National Institute of Aerospace

Sep 2015 – Present Hampton, VA, USA
Member of the NASA Langley Formal Methods Team (Safety Critical Avionics Systems Branch).

Postdoctoral Researcher

University of Malaga

Sep 2014 – Sep 2015 Malaga, Spain
Member of the Mobile Systems and Software Reliability (MORSE) team.

PhD Student

University of Udine

Sep 2010 – Apr 2014 Udine, Italy


Univestitat Politecnica de Valencia

Jan 2010 – Mar 2010 Valencia, Spain



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.


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