Theorem Proving at Work

T. Kobayashi, S. Klikovits, R. Bohrer, A. Yamada, I. Hasuo: Theorem Proving at Work, In Safety Assurance under Uncertainties: From Software to Cyber-Physical/Machine Learning Systems, 1st Edition, CRC Press, chapter 9, pages 41, ISBN 978-1003093350, 2025. Doi: 10.1201/9781003093350

Automotive systems are complex systems. They can exhibit unexpected behaviours, and those unexpected behaviours are often unsafe and can endanger human lives. There are a number of mechanical and control-theoretic methods for automotive safety accumulated over time. However, these traditional measures are rarely enough for modern automotive systems that are heavily software-controlled.