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

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

מקצועות קדם

(234292 - לוגיקה למדעי המחשב ו- 234293 - לוגיקה ותורת הקבוצות למדעי המחשב)


מידע סמסטריאלי