In this talk we will discuss an approach for automating correctness proofs of distributed systems using small model properties and automatic theorem provers. Small model theorems provide bounds on the size of the model that need to be checked for ascertaining the validity of logical formulas. The common theme in this talk is the observation that inductive invariance and progress proof rules, which are arguably the most commonly used techniques in checking correctness of distributed systems, can be expressed in a form that has small model properties. This then makes it is possible to check only finite instances of the system, and infer correctness of arbitrarily large instances. The approach extends to system models with skewed clocks, communication patterns that are regular graphs, as well as models with partial synchrony.
Sayan Mitra is an Associate Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research interests are in formal verification, distributed computing, and cyberphysical systems. He holds a PhD from MIT (2007), MSc from the Indian Institute of Science, Bangalore, and undergraduate degree in EE from Jadavpur University, Kolkata. He was a postdoctoral fellow at the Center for Mathematics of Information of CalTech, and held visiting faculty positions at Oxford University and Kirtland Air Force Research Laboratory. Sayan received the National Science Foundation’s CAREER Award in 2011, AFOSR Young Investigator Research Program Award in 2012, IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award (2013), Samsung Global Research Outreach Award, and several best paper awards.
This talk is organized by Rigorous Systems Engineering (RiSE).