סוג האירוע

בחר הכל

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

מבחן/תחרות

סמינרים

קולוקוויום

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

צהרי יום א'

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

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

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

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

תחום האירוע

בחר הכל

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

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

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

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

ביה"ס לכימיה

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

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

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

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

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

The TAU Programming Languages and Systems Seminar - Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly

Ryan Berryhill, University of Toronto

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

Abstract:

In recent years, IC3 has enjoyed wide adoption as an unbounded
model checking engine. The core algorithm works by learning lemmas that, given a safe property, eventually converge to an  inductive proof. Its
runtime performance is heavily dependent upon  “pushing” important lemmas, possibly by discovering additional supporting lemmas. This talk introduces Truss (Testing Reachability Using Support Sets) - an IC3-based algorithm that does just that. Special SAT queries are used to learn relationships between lemmas. When processing a proof obligation, instead of learning new lemmas, the algorithm attempts to promote supporting lemmas to discharge the obligation. Experiments on HWMCC'15 circuits show significant performance gains.

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