This is a past event.

Karem Sakallah, University of Michigan, will present his talk, “Verification of Distributed Protocol Specifications is Decidable” on-campus and virtually on March 24, 2023, from 3-4 p.m. in Rekhi Hall, Room 214.

The talk is part of the Computer Science Colloquium lecture series hosted by the Department of Computer Science.

Sakallah is a professor of electrical engineering and computer science at the University of Michigan. His current research is focused on automating the formal verification of hardware, software, and distributed protocols.

Join the Zoom meeting here: https://michigantech.zoom.us/j/84155758002

Talk Title: Verification of Distributed Protocol Specifications is Decidable

Talk Abstract: This talk describes a pragmatic problem-solving approach aimed at automatically deriving quantified inductive invariants in first-order logic (FOL) that serve as proof certificates for the safety of distributed protocol specifications. Notwithstanding the oft-cited undecidability result of Apt and Kozen, there is ample empirical evidence suggesting that such invariants can be derived algorithmically by careful analysis of a protocol’s structural regularity. In this talk I will show how to derive quantified FOL invariants that reflect a protocol’s spatial symmetry.

This is an ongoing exploration with several open questions. Sakallah will end the talk by highlighting some of these questions and the progress he has made in answering them.

Read more on the blog post: https://blogs.mtu.edu/computing/2023/01/30/cs-colloquium-lecture-karem-sakallah-university-of-michigan/