For me as Santa Claus, delivering the Christmas presents for every child correctly has become more and more difficult with the increasing number of children. I am essentially leading a business at this point, and all my employees are trying to tell me that of the 548,911,253 presents I must deliver this year, it is fine if one or two are delivered to the wrong location or otherwise get lost. After all, other companies also make "minor" errors like that.
But we are not SOME company: For us as Santa's Factory, every child's life matters. To this end we employ so called formal verification to ensure all the presents are delivered to the correct location.
In this talk Santa Claus will reminisce about how this came to be, starting from some of the history and basics of theoretical computer science. Namely theoretical computer science studies finite representations of infinite graphs, and in formal verification we try to create algorithms for problems of the form:
Given a finite representation R of a graph (V,E) and representations of two vertices v,v' in V, check whether v can reach v' in the graph (V,E). We will see two examples of such a "finite representation", namely counter machines, which are Turing-complete, and then petri nets (not Turing-complete), a model of business processes.
Finally, we explain some of the techniques used to formally verify petri nets, like the marking equation, which is an integer linear program that can in many cases prove non-reachability, though there is no guarantee that the marking equation will give a decisive answer.
In case somebody happens to be listening to me reminiscing, there might also be an interactive part to look forward to.
TopMath Talks
Im Rahmen der TopMath-Talks stellen Studierende und Promovierende des TopMath-Programms Teile ihrer Forschung vor. Sie geben einen verständlichen Einblick in ihr Interessensgebiet und ermöglichen es so Studierenden und Mitarbeitern aus unterschiedlichen Forschungsfeldern, ihre mathematische Allgemeinbildung zu erweitern. Die Talks sind öffentlich und dauern ungefähr eine Stunde mit anschließender Diskussion. Jede*r ist willkommen.