Talk "Formal Analysis of Cyber-Physical Systems Using Rewriting Modulo SMT"

by Kyungmin Bae

Fri, 13 June 2025 at 04:00 pm in Glasgow, Scotland

Joint work with: Jaehun Lee and Peter Ölveczky

Abstract: Cyber-physical systems (CPSs) consist of distributed controllers interacting with continuous physical environments. Formal analysis of such systems is challenging due to the need to jointly reason about advanced control programs, continuous dynamics, message-passing communication, and real-time constraints such as message delays and deadlines. In this talk, I introduce a formal analysis approach based on rewriting modulo SMT, which provides a unified framework for faithfully capturing all of these aspects. Distributed controllers are modeled using rewriting modulo equational theories, and continuous dynamics and real-time constraints are represented symbolically using SMT formulas. We develop novel state-space reduction techniques to address the state-space explosion problem that naturally arises in analyzing such models. We apply this approach to several applications, demonstrating that rewriting modulo SMT provides a scalable and expressive foundation for the rigorous analysis of complex CPSs.