  Modern automotive software is highly complex and consists of millions lines
of code. For safety-relevant automotive software, it is recommended to use
sound static program analysis to prove the absence of runtime errors. However,
the analysis is often perceived as burdensome by developers because it runs for
a long time and produces many false alarms. If the analysis is performed on the
integrated software system, there is a scalability problem, and the analysis is
only possible at a late stage of development. If the analysis is performed on
individual modules instead, this is possible at an early stage of development,
but the usage context of modules is missing, which leads to too many false
alarms. In this case study, we present how automatically inferred contracts add
context to module-level analysis. Leveraging these contracts with an
off-the-shelf tool for abstract interpretation makes module-level analysis more
precise and more scalable. We evaluate this framework quantitatively on
industrial case studies from different automotive domains. Additionally, we
report on our qualitative experience for the verification of large-scale
embedded software projects.
