Time+Place: Tuesday 13/06/2017 14:30 Room 337 Taub Bld.
Title: Effective deductive verification of safety of distributed protocols in unbounded systems
Speaker: Mooly Sagiv - COLLOQUIUM LECTURE - RESCHEDULED https://www.cs.tau.ac.il/~msagiv/
Affiliation: Tel-Aviv University, School of Computer Science
Host: Yuval Filmus


Safety of a distributed protocol means that the protocol never
reaches a bad state, e.g., a state where two nodes become leaders in
a leader-election protocol.
Proving safety is obviously undecidable since such protocols are run
by an unbounded number of nodes, and their safety needs to be
established for any number of nodes.
I will describe a deductive approach for proving safety, based on
the concept of universally quantified inductive invariants --- an
adaptation of the mathematical concept of induction to the domain of
In the deductive approach, the programmer specifies a candidate
inductive invariant and the system automatically checks if it is
By restricting the invariants to be universally quantified, this
approach can be effectively implemented with a SAT solver.

This is a joint work with Ken McMillan (MSR), Oded Padon (TAU),
Aurojit Panda (Berkeley), and Sharon Shoham(TAU) and was integrated
into the IVY system

The work is inspired by Shachar Itzhaky's thesis available from

Short Bio:
Mooly Sagiv is a professor in the School of Computer Science at Tel-Aviv 
University. He graduated from the Technion in 1991. He is a leading researcher 
in the area of large scale (inter-procedural) program analysis, and one of the 
key contributors to shape analysis. His fields of interests include programming
languages, compilers, abstract interpretation, profiling, pointer analysis, 
shape analysis, inter-procedural dataflow analysis, program slicing, and
language-based programming environments. Sagiv is a recipient of a 2013 senior 
ERC research grant for Verifying and Synthesizing Software Composition. 
Prof.  Sagiv served as Member of the Advisory Board of Panaya Inc acquired by 
Infosys. He received best-paper awards at PLDI'11 and PLDI'12  for his work on 
composing concurrent data structures and a ACM SIGSOFT Retrospective Impact 
Paper Award (2011) for program slicing. He is an ACM fellow and a recipient of 
Microsoft Research Outstanding Collaborator Award 2016.

Refreshments will be served from 14:15
Lecture starts at 14:30