research

My main research interests correspond to Software Engineering, in particular formal approaches to Software Engineering. Within this field, I work on various topics, some of which I describe below:

Automated Analysis of Source Code and Formal Specifications

This is currently one of my main lines of research. My work centres around the use of SAT solving to analyse source code or software models. The DynAlloy tool, originally developed by Juan Pablo Galeotti, is a main tool used for various analyses such as:

• Bounded verification of annotated source code
• Validation and verification of software requirements specifications (e.g., SCR, Clafer)
• Automated generation of unit tests

Foundations of Formal Specification Languages

This is the line of work that I pursued during my PhD. I recently got engaged in it again, thanks to collaborations with Pablo Castro, Carlos López Pombo and Tom Maibaum. Our work is on the definition of formal foundations, based on category theory, for different aspects of formal specification languages, including specification structuring, refinement and dynamic reconfiguration.