The papers “Verifying Auto-Generated C Code from Simulink” by Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez and Thomas Rambow, as well as the paper “Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations” by Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham and Joost-Pieter Katoen, have been accepted for the Formal Methods 2018 symposium. Both papers report on results obtained in joint projects with Ford Motor Company.