You are here

Upcoming Seminars

ThursdayJan 18, 201811:00
Guest SeminarRoom 155
Speaker:Shaull Almagor Title:Automated Verification of Infinite-State Systems with Certifiable AlgorithmsAbstract:opens in new windowin html    pdfopens in new window

In formal verification, one uses mathematical tools in order to prove that a system satisfies a given specification.
In this talk I consider three limitations of traditional formal verification:
The first is the fact that treating systems as finite-state machines is problematic, as systems become more complex, and thus we must consider infinite-state machines.
The second is that Boolean specifications are not rich enough to specify properties required by today's systems. Thus, we need to go beyond the Boolean setting.
The third concerns certifying the results of verification: while a verifier may answer that a system satisfies its specification, a designer often needs some palpable evidence of correctness.

I will present several works addressing the above limitations, and the mathematical tools involved in overcoming them.

No prior knowledge is assumed. Posterior knowledge is guaranteed.