Daniel Larraz

Photo of Daniel Larraz

I am a postdoctoral research scholar 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 Kind2.

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.


Teaching Assistant

Programming Languages at UPC, (2014-2015, Bachelor in Informatics Engineering).


Email: daniel-larraz at (replace at with @) uiowa.edu
Phone: +1-319-353-2547
Office: 201N MLH

Mailing address:
Department of Computer Science
The University of Iowa
14 MacLean Hall
Iowa City, IA 52242

Last updated: March 8, 2017