Research

My research is focused in the application of formal methods to verification of software. In particular to apply the well known model checking technique to software systems (Software Model Checking).

Within software model checking I am interested in three main lines:
-Verification of software that makes use of well defined APIs: Development of methods to properly analyze software that uses external functions to the language.
-Dynamic memory verification: Construction of dynamic memory models to represent the heap of programs using dynamic memory, that allows us to verify temporal properties to ensure the correctness of operations over the heap.
-Dynamic data structures analyze: Combination of temporal logics to use model checking technique to analyze both the shape and content of dynamic data structures when analyzing programs. In this topic, the use of CTL and mu-calculus logics allows to analyze complex properties over recursive data structure like list or trees.