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, and virtually.
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.
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. I will end the talk by highlighting some of these questions and the progress we have made in answering them.
Speaker Biography: Karem A. Sakallah is a professor of electrical engineering and computer science at the University of Michigan. He received a B.E. degree in electrical engineering from the American University of Beirut and M.S. and Ph.D. degrees in electrical and computer engineering from Carnegie Mellon University.
Prior to joining the University of Michigan, he headed the Analysis and Simulation Advanced Development Team at Digital Equipment Corporation. Besides his academic duties, he has served in a variety of professional roles including the establishment of a computing research institute in Qatar for which he took a leave to serve a term of three years as the Chief Scientist.
His current research is focused on automating the formal verification of hardware, software, and distributed protocols. He is a fellow of the IEEE and the ACM and a co-recipient of the prestigious Computer-Aided Verification Award for “Fundamental contributions to the development of high-performance Boolean satisfiability solvers.”