Shaull Almagor - CS-Lecture
Thursday, 27.12.2018, 10:30
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.
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.