[Pl-seminar] Reminder: 3/31 Seminar: Mooly Sagiv, Simple Invariants for proving the safety of distributed protocols and networks

[Daniel Patterson]

Reminder - this is next week.

On Mon, Mar 20, 2017 at 9:39 AM Daniel Patterson <dbp at ccs.neu.edu> wrote:

> NUPRL Seminar presents
>
> Mooly Sagiv
> Tel Aviv University
> Host: Jan Vitek and Frank Tip
>
> 12:00-1:30PM
> Friday, March 31st, 2017
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
>
> Simple Invariants for proving the safety of distributed protocols and
> networks
>
> 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/
>
> Bio:
>
> Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv
> University. 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.
>
-------------- next part --------------
HTML attachment scrubbed and removed