סילבוס

תוכן הקורס ומטרתו

הקורס יעסוק באימות אוטומטי של מערכות חמרה ותכנה באמצעות בדיקת מודל (Model Checking).
נציג מספר לוגיקות טמפורליות (CTL*, LTL, CTL) ונדון במידול מערכות ומפרטיהן באופן פורמלי ע"י נוסחאות בלוגיקה טמפורלית, נציג אלגוריתמי בדיקת מודל לבדיקה אוטומטית כי מערכת מקיימת מפרט נתון, נדון במגבלות של האלגוריתמים הללו ובדרכים להתמודד איתן. בפרט, נגדיר יחסי סדר ושקילויות בין מודלים, נציג טכניקות אבסטקרציה ועידון, אימות מודולרי, בדיקת מודל סמבולית מבוססת BDD ובדיקת מודל מבוססת SAT.