Formal methods
In software systems, errors may have catastrophic consequences, especially in systems that are critical for security, such as medical or aerospace programmes. Code checks and reviews may reduce the error rate, but in some cases, a higher security level is required. With this purpose, the formal methods form part of a category of techniques that analyse a mathematical description of the system in order to guarantee its accuracy. Some of the techniques used for formal software verification are model checking, theorem demonstration and static analysis. One problem that all these methods share is the high degree of computational complexity, which may limit applicability in real-world examples. This line of research takes pragmatic approaches into account in order to guarantee the software systems' quality on an industrial scale, and explores key topics such as usability, efficiency and applicability.
Model-driven engineering
Model-driven development is a paradigm that fosters the use of software models in all program design tasks (direct engineering, reverse engineering, interoperability...), as is customary in all the other engineering disciplines. For example, it tries to reduce development costs by focusing more on the creation of software models (specified in UML or using domain-specific languages) than on the code and, after validating these models, it uses code generation tools to automatically generate final implementation of these models. In this research line, we explore techniques and tools for supporting all aspects of model-driven engineering, including handling of very large models, heterogeneous models, collaborative modelling and model discovery (from API to source code).
Software analytics
Software analytics is the study of all the data related with programs and their engineering processes, with the goal of improving understanding of how the software is built. The goal is to be able to predict and improve important quality factors of software artefacts and ascertain the best practices used in previous projects (both those that have been successful and those that have not). In order to learn these factors, mass mining of software repositories such as GitHub (with more than 50 million projects at present) has been undertaken. Software analytics includes the analysis of the program's code, but we are particularly interested in studying all the related social and collaborative aspects (which community builds the software, how does it organize itself, what best practices do they follow, etc.). Recently, we have also started to study the use of bots (virtual assistants) to assist in the automated management of these communities.
