The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
he widespread deployment of computing devices that manage and control physical processes in safety critical environments, has made their analysis and verification a very important problem. Since formal models that disregard the physical processes tend to be conservative and suboptimal, the most popular way to model and analyze such systems is using hybrid systems, that have finitely many control states to model discrete behavior and finitely many real valued variables that evolve continuously with time to model the interaction with the physical world. Despite considerable progress in the last couple of decades, the automated verification of cyber physical systems remains stubbornly challenging. In this talk we will discuss one approach to making the analysis more scalable, namely, by automatically constructing "simpler", "smaller" models, and then analysing these approximated models. We will present a couple of techniques to approximate hybrid models, based on the Stone-Weierstrauss Theorem and counter-example guided abstraction-refinement (CEGAR), and discuss their applications to automated verification.