סוג האירוע

בחר הכל

הרצאות פומביות

מבחן/תחרות

סמינרים

קולוקוויום

כנסים וימי עיון

צהרי יום א'

ימים פתוחים וייעוץ

טקסים ואירועים מיוחדים

הרצאות לקהל הרחב

מועדון קשרי אקדמיה-תעשייה

תחום האירוע

בחר הכל

הפקולטה למדעים מדויקים

ביה"ס למדעי המתמטיקה

ביה"ס לפיזיקה ולאסטרונומיה

המועדון האסטרונומי

ביה"ס לכימיה

מרכז לחקר אינטראקציות אור חומר

סימפוזיונים והרצאות מיוחדות

החוג למדעי כדור הארץ

ביה"ס למדעי המחשב

קולוקוויום בביה"ס למדעי המחשב - Simple Invariants for proving the safety of distributed protocols and networks

Mooly Sagiv

25 ביוני 2017, 11:00 
בניין שרייבר, חדר 006 
קולוקוויום במדעי המחשב

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 environmentsSagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. ProfSagiv 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.

 

אוניברסיטת תל-אביב, ת.ד. 39040, תל-אביב 6997801
Developed by
UI/UX Basch_Interactive