אימות פורמלי של מערכות לימודי הנדסת תוכנה לתואר ראשון .B.Sc

אימות פורמלי של מערכות




Formal Verification of Systems
קוד הקורס: 12021
3 נ"ז

 

מטרות הקורס
הכרת הגישה הנוכחית לבדיקה של מערכות. הבנה איך מבעיה אמיתית עוברים לבעיה מתמטית, וממנה לפתרונות אלגוריתמיים.

נושאי הקורס
לוגיקה טמפורלית. מבני קריפקה, וכיצד מתארים איתם מערכות. שימוש בסיסי ב-model-checker חינמי. שיטות לבדיקת נוסחאות LTL פשוטות. שיטה לבדיקת כל נוסחאות ה-LTL.
בעיית "פיצוץ האוכלוסין" של המצבים במבני הקריפקה, והרעיון של תיאור סימבולי. הבסיס של Bounded model Checking. השיטה הכללית – Bounded model Checking. הרחבת השיטה לשימוש באינדוקציה. פתרון בעיות SAT. האלגוריתם הבסיסי DPLL. שיפור ראשון:watched literals. שיפור שני: למידת פסוקיות.

דרישות הקדם והדרישות המקבילות הינן:
דרישות קדם: חישוביות וסיבוכיות (10076), אלגוריתמיקה 1 (10007).
דרישות מקבילות: אין

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

לייעוץ אקדמי אישי מלאו פרטיכם

צור איתנו קשר »

אני מאשר/ת קבלת מידע פרסומי מהמכללה

מוזמנים להתייעץ איתנו