El investigador de Instituto IMDEA Software Aleks Nanevski recibe la prestigiosa financiación ERC Consolidator Grant para llevar a cabo el proyecto “Mathador - Type and Proof Structures for Concurrent Software Verification”.
Escribir programas concurrentes entraña mucha dificultad dada la complejidad de las interacciones entre sus componentos. Esta complejidad aumenta cuando uno trata de desarrollar pruebas matemáticas, automaticamente verificables, que demuestren que el programa produce el resultado deseado. Hoy en día desarrollar este tipo de pruebas requiere un considerable esfuerzo incluso para los programas más simples debido a la explosión combinatórica asociada a la complejidad de las interacciones entre componentes.
El objetivo del proyecto Mathador es estudiar, descomponer y simplificar la estructura de pruebas para programas concurrentes, de tal manera que puedan ser facilmente producidas. Este resultado ayudará a nuestra comprensión de las interacciones entre componetes concurrentes, y cambiará la manera en la que pensamos, escribimos, y entendemos el software concurrente.
Más información: Comunicado de prensa de ERC y Lista de beneficiarios de la beca ERC Consolidator Grant.
