סוג האירוע

בחר הכל

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

קולוקוויום

סמינרים

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

מועדון IAP

מבחן/תחרות

צהרי יום א'

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

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

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

תחום האירוע

בחר הכל

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

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

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

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

ביה"ס לכימיה

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

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

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

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

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

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

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

The TAU Programming Languages and Systems Seminar - Property Directed Self Composition

Ron Shemer 

26 במאי 2019, 12:30 
בניין שרייבר, חדר 309 
הרצאה לקהל הרחב

Abstract:

 

We address the problem of verifying k-safety properties: properties that refer to k interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the original program is reduced to checking an "ordinary'' safety property over a program that executes k copies of the original program in some order. The way in which the copies are composed determines how complicated it is to verify the composed program.

We view this composition as provided by a semantic self composition function that maps each state of the composed program to the copies that make a move.

Since the "quality'' of a self composition function is measured by the ability to verify the safety of the composed program, we formulate the problem of inferring a self composition function together with the inductive invariant needed to verify safety of the composed program, where both are restricted to a given language.

We develop a property-directed inference algorithm that, given a set of predicates, infers composition-invariant pairs expressed by Boolean combinations of the given predicates, or determines that no such pair exists.

We implemented our algorithm and demonstrate that it is able to find self compositions that are beyond reach of existing tools.

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