Computer Sciences Colloquium - Certifiable Algorithms in Automated Verification

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.