About
I've earned my Ph.D. in Computer Science at the University of Buenos Aires in 2014, under the supervision of Marcelo Frías. I joined the National Institute of Aerospace as a Postdoc shortly after that, and I am still working there as a Senior Research Scientist. I have always tried to facilitate and ease the construction and verification of safer systems by applying Formal Methods in the different stages of their life cycle. I am currently conducting research on formal verification of safety-critical systems with the NASA Formal Methods Group at NASA Langley.
Download my cvActive Interests
Interactive Theorem Proving
Handcrafting syntactic truth since c. 2006. My poison of choice is the Prototype Verification System. I contribute to the prover and, more regularly, to its de-facto library: NASALib.
Formal Analysis of Programs
Lately, focused on the verification of floating-point programs, with particular emphasis on providing externally verifiable certificates about the correctness of the analysis.
Automating Interactive Provers
I've been participating in a collaborative effort to implement several termination criteria in PVS, which also involved their actual formalization. I'm also trying to provide PVS with an automatic counterexample generator based on SAT-solving.
