Bit-precise formal verification of discrete-time MATLAB/Simulink Models using SMT Solving

Matlab/Simulink is widely used for model-based development of embedded systems. In particular, safety-critical applications are increasingly designed in Matlab/Simulink. At the same time, formal verification techniques for Matlab/Simulink are still rare and existing ones do not scale well. In this paper, we present an automatic transformation from discrete-time Matlab/Simulink to the input language of UCLID. UCLID is a toolkit for system verification based on SMT solving. Our approach enables us to use a combination of bounded model checking and inductive invariant checking for the automatic verification of Matlab/Simulink models. To demonstrate the practical applicability of our approach, we have successfully verified the absence of one of the most common errors, i. e. variable over- or underflow, for an industrial design from the automotive domain.