אימות תוכנה

חלק א': הוכחת נכונות: תוכניות תרשימי זרימה, תוכניות WHILE, שיטות FLOYD ו-HOARE להוכחת נכונות חלקית ועצירה.

חלק ב': בדיקת מודל : לוגיקות טמפורליות: LTL, CTL, CTL*, בדיקת מודל CTL, הוגנות. התפוצצות מצבים, טכניקות מבוססות BDD. בדיקת מודל סימבולית, בדיקת מודל מבוססת SAT.

דרישות הקדם והדרישות המקבילות בקורס אימות תוכנה הינן:

דרישות קדם: מפרטים פורמליים  לתיאור מערכות (10043), לוגיקה מתמטית (10019), אלגוריתמיקה 2 (10008)

דרישות מקבילות: אין

לחצו למעבר אל תוכנית לימודי הנדסת תוכנה