Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Certifiable Algorithms in Automated Verification
event speaker icon
Shaull Almagor - CS-Lecture
event date icon
Thursday, 27.12.2018, 10:30
event location icon
Room 601 Taub Bld.
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.