פורטל הסטודנטים

הסמינר יעסוק באלגוריתמים מתקדמים לאימות פורמלי. הנושאים יכללו: רדוקציה של בעיית האימות לספיקות פסוקיות הורן, שיטות לפתרון בעיית הספיקות עבור פסוקיות הורן, שימוש בהייפר-תכונות (HYPER-PROPERTIES) לאימות והשיטות השונות לפתרון שלהן._ תוצאות למידה: בסיום הקורס הסטודנטיות והסטודנטים ילמדו ויכירו מחקר חדשני שנמצא בחזית בתחום האימות הפורמלי. - כיצד לייצג את בעיית אימות התוכנה כמערכת פסוקיות הורן. - אספקטים שונים בבעיית ספיקות של פסוקיות הורן מעל תאוריות של לוגיקה מסדר ראשון._ - אלגוריתמים חלקיים לפתרון בעיית הספיקות של פסוקיות הורן בלוגיקה מסדר ראשון המבוססים על אלגוריתמי בדיקת מודל._5 - יכירו הייפר-תכונות ואת השימושים השונים עבור אימות תכונות מורכבות._5 - יכירו שיטות שונות לרדוקציה של הייפר-תכונות לתכונות בטיחות בלוגיקה טמפורלית. - יכירו הייפר תכונות עם חילופי כמתים, יבינו את הסיבוכיות של הבעיה ושיטות לפיתרון.

פקולטה: מדעי המחשב
|תואר ראשון |תארים מתקדמים

מקצועות קדם

(234292 - לוגיקה למדעי המחשב ו- 236342 - מבוא לאימות תוכנה)