Lost in Translation: Formal Methods vs. Industrial Reality

Speaker

Andrea Flexeder

Affiliation

Robert Bosch GmbH

Type

Industrial Talk

Abstract

The theory is elegant. The codebase is not. Automotive software arrives as a heterogeneous mix: hand-written C sitting next to model-generated code from MATLAB/Simulink and AUTOSAR, SW components decoupled from function development artifacts, and code old enough to have its own ISO standards.

Tools like Astrée and Polyspace enter with mathematical certainty. The code is less convinced.

The walls are real: complexity, scale, certification pressure, and the annotation burden that formal tools silently impose on a development world that was never built to be verified. Formally speaking, the problem is well-defined. Practically speaking, good luck.

Decades of trying to make formal methods work at automotive scale. Still not there.

Can GenAI finally take on the engineering effort that formal tools pre-suppose but never provide – or are we just translating the same problem into a new language?