For the next seminar, we will have the pleasure of welcoming Sergio Mover who has recently joined us in the Cosynus team.

Abstract: Hybrid systems can model complex systems that we have to trust (e.g., the landing gear subsystem of on an airplane) and where software interacts with the physical environment. In this seminar, I will mainly focus on an automatic formal verification technique for Hybrid Systems that is based on a reduction to discrete, but still infinite states, transition systems. I will first explain the first-order logic formalism used to represents discrete systems and verification algorithms based on Satisfiability Modulo Theories (SMT). I will then describe the reduction of (subclasses of) hybrid systems to discrete systems and show different applications of the approach. Then, I will briefly switch topic and introduce an ongoing research project, Fixr, where we tackle the problem of exploiting existing “program artifacts” (e.g., source code, execution traces) to build assistive technology (e.g., similar code search, bug finding, automatic bug repair). I will conclude discussing some future research directions.