The Taub Faculty of Computer Science Events and Talks

In formal verification, one uses mathematical tools in order to prove that a system satisfies a given specification. A limitation of traditional formal-verification algorithms and tools concerns the certification of positive results: while a verifier may answer that a system satisfies its specification, a designer often needs some palpable evidence, or certificate, of correctness. I will discuss the notion of certificates in several applications of formal verification, and present two works addressing the above limitation in different settings: the first considers multi-agent robotic planning, and the second considers reachability analysis in discrete linear dynamical systems. Through these works, I will demonstrate the rich variety of mathematical and algorithmic tools involved in overcoming the limitation above, which range from elementary graph algorithms to deep results in number theory. No prior knowledge is assumed, posterior knowledge is guaranteed. Short Bio: ============ Shaull Almagor is a postdoctoral researcher at Oxford University. He obtained his PhD in 2016 from the Hebrew University. His research interests include formal methods, weighted automata, quantitative logics, dynamical systems, and robotic planning.