עמדות מחשבים במעבדה להנדסת תוכנה

הנדסת תוכנה

אוטומטים ושפות פורמליות




קוד קורס: 10087
2.5 נ"ז

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

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

דרישות קדם: אלגוריתמיקה 2 (10008), לוגיקה מתמטית (10019).
דרישות מקבילות: אין.

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

שיתופי פעולה: