Conferencia impartida David Sanán, profesor del Singapore Institute of Technology (SIT).

 

Título:

Correctness of IoT and AV Systems by Using Compositional Techniques for the Verification of Concurrent Software

 

Resumen:The increasing presence of IoT devices and Autonomous Systems (from drones to cars) in our lives has brought significant concerns regarding the correctness of such systems. The verification of applications in these domains requires expressive languages and techniques to tackle their complexity and handle the concurrency of the software running on multi-core architectures.

In this talk, I will introduce compositional methodologies for the scalable verification of concurrent software and the verification of two systems using these techniques: the memory management of Zephyr, an OS for the IoT, and a state-of-the-art micro-kernel used in the aerospace domain aiming at multi-core architectures.

Short bio: David cursó sus estudios de ingeniería informática en la Universidad de Málaga, donde obtuvo su Ph.D. en 2009, y desde el año 2011 ha estado investigando en universidades de Europa y Asia tales como Trinity College Dublin, National University of Singapore y Nanyang Technological University. Su principal línea de investigación es la aplicación de métodos formales en sistemas críticos, con especial énfasis en security micro-kernels para arquitecturas hardware con varios procesadores. En este área, David ha trabajado en el desarrollo de semánticas, lógicas y herramientas que hagan posible la verificación de estos security micro-kernels. Otras aplicaciones en las que también está interesado son Quantum Computing y Smart Contracts.

 

Puede serguirse online en el siguiente enlace