Klaus von Gleissenthall

Date: 17:00, Thursday, September 17, 2015
Speaker: Klaus von Gleissenthall
Venue: IST Austria

The cardinality operator is indispensable when specifying and
reasoning about parameterized concurrent/distributed systems. It
provides a level of abstraction and conciseness that makes (manual)
proofs go through smoothly. Unfortunately, the automation support for
such proofs remains elusive due to challenges in counting sets of
unbounded program states.  In this talk, I will present #Π a tool that
can automatically synthesize cardinality-based proofs of parameterized
systems. #Π crucially relies on a sound and precise axiomatization of
cardinality for the combined theory of linear arithmetic and
arrays. This axiomatization is the key technical contribution of this
work.  We show that various parameterized systems, including mutual
exclusion and consensus protocols, can be efficiently verified using
#Π. Many of them were automatically verified for the first time. This
is joint work with Nikolaj Bjørner and Andrey Rybalchenko.

Posted in RiSE Seminar