Thomas Kropf
President of corporate research and advance engineering at Bosch
Real-time systems engineering @ Bosch – From research to industry and back (slides)
Bio:
Thomas Kropf has held various management and engineering positions within Bosch in the areas of microelectronics, driver assistance, chassis systems, and infotainment. He studied electrical engineering and holds a Ph.D. in computer science. Besides his main duty at Bosch, he is an adjunct professor for computer science at the University of Tübingen.
Abstract: Bosch is a leading provider of real-time critical cyber physical systems in various domains such as automotive, manufacturing, home & building automation, and robotics. Thus, Bosch is using a lot of technology originating from the real-time systems research community as well as actively contributing to the community, e.g. by publishing benchmark models and posing challenges. This talk will highlight some of the current industrial trends and challenges Bosch is facing as well as some solution approaches currently being investigated at Bosch.
David Monniaux
Senior researcher at CNRS/Verimag
Some industrial applications I’ve been involved in (slides)
Bio:
David Monniaux is the head of the PACSS team (Proofs and Code analysis for Safety and Security) at Verimag. He works on static analysis by abstract interpretation, algorithmics of abstract interpretation and decision procedures, as well as certified compilation. He was one of the main developers of the Astrée and Verasco static analyzers.
Abstract: Designers of safety-critical systems have to ensure these systems behave as intended. In certain application domains (e.g. avionics at the highest safety levels), this is an onerous and ponderous process. I will discuss my personal experience with two projects: 1) ASTRÉE: a tool for automatically proving that programs do not have undefined behaviors (accesses out of bounds, overflows…). 2) CompCert: a compiler for which there is a mathematical proof that the assembly code is a faithful translation of the source code. Both tools, arising from French academic projects, are now commercialized by Absint GmbH.