Mooly Sagiv - COLLOQUIUM LECTURE - RESCHEDULED
Tuesday, 13.6.2017, 14:30
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
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