I am an Associate Professor in the Department of Electronics and Computer Science at the Pontificia Universidad Javeriana, in Cali (Colombia), where I am involved in Formal Methods research and teaching.

I earned a B.S. degree and a M.Sc. degree in Informatics from the Universidad de los Andes (Colombia). During my master studies and under the supervision of Rubby Casallas and Rafael García in the Software Construction Group, I designed a formal calculus for service assemblage and component composition based on the pi-calculus. This formal calculus was useful in giving formal semantics to Gaita, a model of services and components. During my undergraduate studies I advanced a small research project called Java-: An Axiomatic Semantics for a Concurrent Subset of Java, under the supervision of Rodrigo Cardoso.

I attended the University of Illinois at Urbana-Champaign where I earned a Ph.D. degree in Computer Science from the Department of Computer Science under the supervision of Prof. José Meseguer from the Formal Methods and Declarative Languages Laboratory, and a M.Sc. in Mathematics from the Department of Mathematics. My doctorate research focused on symbolic reachability analysis techniques for rewrite theories; my dissertation titled "Symbolic Reachability Analysis for Rewrite Theories" proposes narrowing, SMT, and tree automata -based techniques and tools for symbolic reachability of rewrite theories. These techniques have been successfully applied to a broad class of case studies.

I often work as a software architect/consultant in Colombia's public and private sector. I have been involved in at least 8 large scale successful software projects.