Boolean Satisfiability Modulo Differential Equation Simulations

Speaker: Tomáš Kolárik, Czech Technical University in Prague, Czech Republic 

Abstract: Differential equations are of immense importance for modeling physical phenomena,
often in combination with discrete modeling formalisms. In current industrial practice, properties of the resulting models are checked by testing, using simulation tools.
Research on SAT solvers that are able to handle differential equations has aimed at replacing tests by correctness proofs. However, there are fundamental limitations to such approaches in the form of undecidability, and moreover, the resulting solvers do not scale to problems of the size commonly handled by simulation tools. Also, in many applications, classical mathematical semantics of differential equations often does not correspond well to the actual intended semantics, and hence a correctness proof wrt. mathematical semantics does not ensure correctness of the intended system. We head at overcoming those limitations by an alternative approach to handling differential equations within SAT solvers. This approach is based on the semantics used by tests in simulation tools, but still may result in mathematically precise correctness proofs wrt. that semantics.

Biography: Tomáš Kolárik holds a MSc degree from the Faculty of Information Technology, Czech Technical University in Prague (FIT CTU) in design and verification of embedded systems. Currently he is finishing his PhD studies at FIT CTU in the area of formal verification. Tomáš is a C++ and Linux geek and a sport and board games enthusiast.

Host: Prof. Natasha Sharygina