My main research interest is on Program Analysis and Verification. In
general, I am interested on applying static program analysis techniques for
inferring runtime program properties. So far, I have focused on
inferring complexity bounds of sequential imperative programs:
- I have developed techniques for inferring precise worst-case and best-case complexity
bounds
- The applied techniques are based of symbolic computation and
static analysis
I also have obtained some theoretical complexity results (together
with my co-authors) on the termination property of some simple
loops. Mainly, I have shown that
- Termination of some simple loops are undecidable
- Termination of some other simple loops have EXPSPACE-hard lower bound
At present, I am working on the expressiveness of some abstract
program models with respect to some program properties, trying to
understand the theoretical limits of the respective models and
possible minimal extensions of these models in obtaining sound and precise
program properties. I am also interested on program termination, and algorithmic
verification of concurrent programs. More information can be found in
my research statement.
Program Analysis, Static Analysis, Termination, Software Verification, Abstract Interpretation,
Program Synthesis, Theorem proving, Program Semantics