IMDEA Software Institute Research

The research activities carried out by the IMDEA Software Institute address directly its core mission: to advance the scientific and technological foundations that will allow the cost-efficient development of software characterized by sophisticated functionality and high quality, in terms of safety, reliability, and efficiency. We pursue our mission by focusing on three strategic areas, namely Security and Privacy, Program Analysis and Verification, and Languages, Compilers, and Systems:

• Our research on Security and Privacy delivers technology that enables computation, communication, and storage in open, untrusted, and malicious environments, such as the Internet of Things. Our results include novel cryptographic protocols and privacy-enhancing technology, as well as cutting-edge techniques for detecting and analyzing vulnerabilities and malicious activities in software, hardware, and network traffic.

  This area is covered by: Gilles Barthe, Juan Caballero, Dario Fiore, Alessandra Gorla.

• Our research on Program Analysis and Verification advances the foundations and the tools that enable software engineers understand the key properties of the complex systems they are building. Our results range from tools that automatically establish proofs of correctness and safety, which is paramount, for example, for avionics and automotive software, to tools that explore energy consumption profiles at design time, which is fundamental for cost-effective software development in the mobile and embedded domains.

  This area is covered by: Gilles Barthe, Juan Caballero, John Gallagher, Pierre Ganty, Alexey Gotsman, Alessandra Gorla, Manuel Hermenegildo, Niki Vazou, Pedro López, José Francisco Morales, Aleks Nanevski, César Sánchez.

• Our research on Languages, Compilers, and Systems provides software engineers with the means they need to describe their ideas in more concise and modular ways and to generate correct and performant executables from these descriptions, and with platforms on which these programs can run efficiently. Progress in this area has the potential to dramatically increase programmer productivity as well as maintainability and reusability of software. Our results include powerful multi-paradigm programming environments, novel language-based techniques for building highly efficient and provably secure concurrent and distributed systems.

  This area is covered by: Gilles Barthe, Manuel Carro, John Gallagher, Manuel Hermenegildo, Niki Vazou, Pedro López, José Francisco Morales, Aleks Nanevski, César Sánchez.

All these areas develop work in with two complementary dimensions:

• Tools, in different degrees of maturity, that help automate the process of generating high-quality software. These are fundamental to reach the objective of technological transfer to industry.

• Foundations, which lay the rigorous basis for practical and sound methodologies and tools that can be used with high confidence in production environments.

More details available in the latest Annual Report. Alternatively, visit the homepage of the researcher covering the area of your interest.