USI - Email

Archive / INF Seminars / INF_2023_10_10_TomasKolarik

USI - Email

	Boolean Satisfiability Modulo Differential Equation Simulations

Host: Prof. Natasha Sharygina

Tuesday

10.10

USI East Campus, Room D1.13

10:00 - 11:00


	Tomáš Kolárik CTU Prague, Czech Republic

Abstract: Diﬀerential 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 diﬀerential 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 diﬀerential 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 diﬀerential 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.