Sayan Mitra

Date: 17:30, Thursday, December 10, 2015
Speaker: Sayan Mitra
Venue: TU Wien

Time: 17:30

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.

Posted in RiSE Seminar