Park, JunkilLee, InsupPappas, George JPajic, MiroslavSokolsky, Oleg2023-05-222023-05-222015-10-012015-10-15https://repository.upenn.edu/handle/20.500.14332/6877We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller’s state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller’s transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.© ACM 2015. This is the author's version of the work. It is posted here for your personal use. Not for redistribution.CPS Model-Based DesignCPS Formal MethodsCPS Embedded ControlComputer EngineeringComputer SciencesPresentation