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
As part of the TopMath talks, TopMath students and doctoral students present parts of their research. They provide an understandable insight into their current area of interest, enabling students and staff from different research fields to broaden their mathematical background knowledge. The talks are open to the public and last about an hour, followed by discussion. You are cordially invited!