Automatic Verification of Distributed Protocol Specifications

Abstract: Most approaches for the automated verification of distributed protocols center on deriving an inductive invariant for a specific safety property S. In this talk, I present an alternative approach for a restricted yet important class of protocols: leveraging inherent structural symmetry to derive a unique, property-independent formula R that precisely captures the reachable states as a minimum-cost conjunction of quantified first-order logic predicates. For finite instances, these predicates correspond to symmetry orbits of prime implicates, computed via a novel SAT-based logic minimization algorithm that exploits the complementary nature of symmetry and quantification. Empirically, minimum-cost orbits computed at increasing protocol sizes converge syntactically to a fixed point at a small Reachability Cutoff size, confirming earlier observations about cutoff and saturation phenomena. To our knowledge, this is the first method to algorithmically derive exact, quantified first-order reachability formulas for unbounded parameterized systems, allowing any safety property S to be verified by a simple implication test (R ==> S).

Bio: Karem Sakallah is a professor of Electrical Engineering and Computer Science at the University of Michigan. His research focuses on developing tools for the automated, scalable verification of hardware and software systems. He is best known for developing the GRASP SAT solver, which introduced the conflict-driven clause learning (CDCL) algorithm foundational to modern SAT solvers. His current research seeks simple, automated solutions for verifying unbounded parameterized systems by exploiting their inherent regularity. Beyond his research and teaching, he co-founded the Qatar Computing Research Institute (QCRI) and served for a few years as its Chief Scientist. He is a Fellow of both the IEEE (Life Fellow) and the ACM.

Website: https://web.eecs.umich.edu/~karem/