סוג האירוע

בחר הכל

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

קולוקוויום

סמינרים

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

מועדון IAP

מבחן/תחרות

צהרי יום א'

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

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

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

תחום האירוע

בחר הכל

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

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

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

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

ביה"ס לכימיה

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

פרס סאקלר במדעים הפיזיקליים - כימיה

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

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

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

ביה"ס למדעי כדור הארץ

החוג ללימודי הסביבה

קולוקוויום בביה"ס למדעי המחשב - Deductive verification of distributed protocols in first-order logic

Oded Padon, TAU

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

Abstract:

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, due to the infinite state space (e.g., unbounded number of nodes, messages) and protocols complexity, verification is both undecidable and hard in practice. I will describe a deductive approach for verification of distributed protocols, based on decidable fragments of first-order logic, inductive invariants and user interaction. The use of decidable fragments of first-order logic allows to completely automate some verification tasks. Tasks that remain undecidable (e.g. finding inductive invariants) are solved with user interaction, based on graphically displayed counterexamples. I will also describe the application of these techniques to verify safety of several variants of Paxos, and a way to extend the approach to verify liveness and temporal properties.

 

This work is part of my Ph.D. studies under the supervision of Prof. Mooly Sagiv.

אוניברסיטת תל אביב עושה כל מאמץ לכבד זכויות יוצרים. אם בבעלותך זכויות יוצרים בתכנים שנמצאים פה ו/או השימוש
שנעשה בתכנים אלה לדעתך מפר זכויות, נא לפנות בהקדם לכתובת שכאן >>