Formal methods

Bugs in software systems may have catastrophic consequences, especially in safety-critical systems such as medical or aerospace software. Testing and code reviews can reduce the defect rate, but sometimes a higher level of assurance is required. To this end, formal methods are a series of techniques that analyse a mathematical description of the system in order to ensure its correctness.

Some techniques used in the formal verification of software are model checking, theorem proving and static analysis. A problem shared by these approaches is their high computational complexity, which can limit their applicability in real-world examples. This research line will consider pragmatic approaches for ensuring the quality of software systems at an industrial scale, considering key issues such as usability, efficiency and applicability.

Model-driven engineering

Model-driven development is a paradigm that promotes the use of software models in all software engineering tasks (forward engineering, reverse engineering, interoperability, etc.), as is typical in all other engineering disciplines. For instance, it attempts to reduce development costs by focusing on producing software models (specified in UML or by using domain-specific languages) rather than code, and once those models are validated, it relies on code-generation tools to generate automatically the final implementation based on these models.

In this research line, we investigate techniques and tools to support all aspects of model-driven Engineering, including manipulation of very large models, heterogeneous models, collaborative modelling and model discovery (from APIs or source code).

Software analytics

Software analytics is the study of all data related to software and its engineering processes in order to better understand how software is built. The goal is to be able to predict and improve important quality factors of software artefacts and learn best practices from past projects (both successful and not). The learning of these factors is performed by mining massive software repositories like GitHub (with over 30 M projects at the moment).

Software analytics includes the analysis of the program code, but we are especially interested in the analysis of all the collaboration and social aspects around it (who the community is that builds the software, how they are organized, what best practices they follow, and so on).