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

Abstract:


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
programs. 
In the deductive approach, the programmer specifies a candidate
inductive invariant and the system automatically checks if it is
inductive.
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
http://www.cs.tau.ac.il/~odedp/ivy/

The work is inspired by Shachar Itzhaky's thesis available from
http://people.csail.mit.edu/shachari/

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