FV Time Manager Presentationprivat

emissió: 21 oct. 2020  |  
Comentaris (0)
  • It is a fact that any software of reasonable size contains errors. However, with techniques from formal logic we have been able to produce guaranteed error-free software, with a mathematical proof to this extent.
    This new paradigm of programming is extremely costly and time-consuming. As such, it is only profitable for critical software, for instance in aviation, finance, or legal software.  Our main project involves legal software for road transportation that issues fines and even imprisonment on a fully automated basis. Here, guaranteed correctness of the software is clearly an absolute must.
    As a first step, Dr. Joost J. Joosten and his team present the FV Time Manager, a software that converts and manipulates different time stamps and arithmetical operations on them. This time manager is novel and revolutionary in two aspects: firstly, it is generated from a formally verified source and as such, this source code is guaranteed via a mathematical proof to be error-free; secondly, it incorporates so-called leap seconds, small time variations which most pre-existing time managers have so far ignored, but nonetheless should be accounted for according to the law. The latter has a real impact on road transportation, as shall be shown in the presentation.
    As such, our project is a first step to an unprecedented level of cybersecurity.
    Llicència Creative Commons by-nc-nd
    Alerta de contingut erroniTancar
    Si heu detectat algún error a aquest vídeo ens ho podeu notificar al correu mencionant l'identificador del vídeo: 116573
    ©Universitat de Barcelona
  • Codi per incrustar aquest vídeo