Resumen:
En esta charla daremos una visión general de lo que son los resolutores de restricciones SMT (satisfiability modulo theories) y sus extensiones para optimización. A pesar de tener solo 20 años de historia el uso de la tecnología SMT se ha extendido a una gran variedad de áreas de investigación y de la industria. En la charla mostraremos las principales características de los SMT que justifican su buen comportamiento en una gran variedad de problemas industriales y académicos. En este sentido, aunque la forma de describir las restricciones es importante, una gran ventaja del uso de los resolutores SMT para el usuario es que, en general, no necesitan recurrir a heurísticas especializadas para resolver problemas en ámbitos muy distintos. Presentaremos varios casos de éxito en empresas punteras y detallaremos algunas aplicaciones en las que hemos trabajado. Finalmente, veremos algunas de las limitaciones actuales de estos resolutores y los retos que se presentan para el futuro.
Conferenciante:
Albert Rubio es Catedrático de Universidad desde 2008. Actualmente es miembro del grupo COSTA en la Universidad Complutense de Madrid (UCM) y anteriormente fue profesor en la Universitat Politècnica de Catalunya (UPC, hasta el 2019). Es coautor de un capítulo del Handbook of Automated Reasoning, así como de numerosos artículos en revistas y congresos internacionales de primer nivel, entre los que destacan congresos como LICS, CAV, OOPSLA o el Journal of the ACM. Ha participado en el desarrollo de resolutores y optimizadores SMT dentro del grupo Barcelogic en la UPC y desde hace diez años trabaja en aplicaciones de los resolutores SMT y Max-SMT para el análisis de programas, testing de programas concurrentes, análisis de vulnerabilidades en contratos inteligentes y optimización de código en compiladores. Ha sido ininterrumpidamente investigador principal de proyectos financiados del Plan Nacional desde 2004 y director del comité ejecutivo de la International Termination Competition desde 2009. Actualmente, lidera el desarrollo del compilador de circom 2.0, un lenguaje de programación para circuitos aritméticos que pueden ser usados en pruebas de conocimiento nulo (zero-knowledge proofs) y participa en un proyecto financiado por la Ethereum Foundation, para optimizar el código generado por el compilador de Solidity.
Fecha y hora de celebración:
9 de junio de 2021, 16:00 h.
