I am currently a post-doctoral researcher at the IMDEA Software Institute. My main research area is based in the development and implementation of novel theories and decision procedures capable of dealing with parametrized systems and concurrent data structures.
I joined the IMDEA Software Institute as a research student in September 2009 under the supervision of César Sánchez. As a student, my research comprised the formal verification of temporal properties on concurrent parametrized systems using deductive methods and the development of specialized decision procedures for data structures that manipulate dynamic memory. In September 2015 I received my PhD degree in Computer Science from the Escuela Técnica Superior de Ingenieros Informáticos of the Universidad Politécnica de Madrid in Spain.
Before starting my PhD I was an intern at IMDEA, studying the verification of concurrent programs. Prior to that, I was an intern at the PULSAR (formerly ORION) research team at INRIA's Sophia-Antipolis research center in France, where I worked in the extension of a knowledge representation language based on C++.
Previously, I was a software engineer at Gameloft where I specialized in porting and improving games for mobile devices based on JAVA J2ME technology. I was also software developer at the Cordoba Technology Institute where I was working in clean-room implementations of JAVA libraries as part of the Apache Harmony Java Standard Edition project for the Apache Software Foundation.
Currently I also hold a MS degree in Computer Science Research which I received in 2011 from the Computer Science School of the Complutense University of Madrid in Spain. Previously, in 2007, I received my BS degree in Computer Science from the School of Mathematics, Astronomy and Physics of the National University of Cordoba in Argentina.
For further details, you can download the latest version of my CV from here
My current research is mainly focused on formal techniques
and decision
procedures capable of tackling the verification of temporal properties
on
complex parametrized concurrent systems and data structures. This includes:
Some of the projects I have developed.
I am the main developer and maintainer of LEAP, an interactive theorem prover which aims the verification of safety and liveness properties on concurrent parametrized systems and complex concurrent datatypes using deductive techniques and specialized decision procedures.
You can download LEAP, examples and access more detailed information related to this project at LEAP's website
NEW! Now it is possible to try LEAP online through this website
I have implemented some decision procedures for pointer-based data structures. The decision procedure implementations are built on top of SMT solvers, hence you will need to have Yices (currently the implementation relies on Yices1) and Z3 installed in your system.
Here you can download some binaries of these decision procedures implementations, including some examples:
| Binary for Mac | 5,123 KB |
| Binary for 32-bits Linux | 3,212 KB |
| Binary for 64-bits Linux | 3,808 KB |
| Simple example | 705 B |
| Binary for Mac | 5,691 KB |
| Binary for 32-bits Linux | 3,530 KB |
| Binary for 64-bits Linux | 4,176 KB |
| Simple example | 794 B |
As part of my bachelor's thesis I implemented a prototype of an interactive proof assistant using pure type systems. Here is an standalone for Linux.
Slides of some of the presentations I have given in the last years.