I am a research scientist at the University of Iowa. My research focuses on the application of SMT-based techniques to the formal verification of computer systems. I am currently working with Cesare Tinelli on the development of automated techniques to verify synchronous data-flow programs, and their implementation in the model checker Kind 2.
I obtained my PhD at the Technical University of Catalonia (UPC) under the supervision of Albert Rubio. For my PhD I worked on array invariant generation, termination analysis, and compositional safety verification of imperative programs using Max-SMT solvers. I also contributed to the implementation of the VeryMax tool, a verification framework for checking automatically safety properties, and proving (conditional) termination and non-termination of C/C++ programs.
From April through June 2014, I spent three months as a research intern at Microsoft Research Cambridge in the Programming Principles and Tools group under the supervision of Andrey Rybalchenko.