סוג האירוע

בחר הכל

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

מבחן/תחרות

סמינרים

קולוקוויום

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

צהרי יום א'

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

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

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

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

תחום האירוע

בחר הכל

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

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

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

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

ביה"ס לכימיה

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

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

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

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

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

קולוקוויום בביה"ס למדעי המחשב - EFFICIENTLY REASONING ABOUT PROGRAMS

מרצה המכון ללימודים מתקדמים ע"ש מורטימר וריימונד סאקלר Neil Immerman

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

Abstract

 

When Alan Turing defined his computing machines in his original 1936 paper, he proved that even the simplest problems about their behavior, e.g., does a given machine when started on input 0 eventually halt, was not computable.  Thirty-five years later, Steve Cook presented SAT as the first NP-complete problem.  The understanding was that SAT was an inherently infeasible computational problem.  Now that a large and increasing part of our world is organized and controlled by computer programs, we need as much automatic help as possible to assure that our programs safely and faithfully do what they should do. In this talk, I will describe a language and methodology that has been built up to reason about properties of programs, including the reachability of pointers in programs that destructively update data structures.  We automatically define correctness conditions for these programs.  These are translated to SAT problems and then, in practice, efficiently checked using SAT solvers.

 

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