חיפוש חדש  חזור
מידע אישי לתלמיד

שנה"ל תש"ף

  ניתוח ואימות תוכנה
  Program Analysis and Verification  
0368-4479
מדעים מדויקים
קבוצה 01
סמ'  ב'1500-1800 שיעור ות פרופ רינצקי נעם
דרישות קדם   רשימת התפוצה  
ש"ס:  3.0

סילבוס מקוצר
Operational semantics (How do we formally define the meaning of programs).
Program logics (Classical and modern approaches for manual verification of computer programs).
Abstract interpretation (Theoretical foundation of automatic compile-time
analysis, aka static analysis, For example, determining during compile time whether x= y / z is always 1 or that at this program point z is not zero.)
Miscellaneous verification techniques: MC (Model
checking), SAT (Satisfiability) and SMT (Satisfiability
Modulo Theory).
 
The course will have ~4 exercises and a final project (that can be done in pairs.)
Prerequisite: Computational models (0368-2200)

להצהרת הנגישות


אוניברסיטת ת 1