מבוא לאימות תוכנה

236342

קישור לאתר הקורס

3

2

1

0

1

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

234293  או 234292 

אביב 2020/21(תשפ"א) קיץ 2019/20(תש"ף)

דר. יקיר ויזל

בתאריך 07.02.2021 יום א משעה 9 עד השעה 12

בתאריך 05.03.2021 יום ו משעה 9 עד השעה 12

חדרי בחינה מועדי וחדרי בחנים