דילוג לתוכן ראשי

קורסים

  • מודלים חישוביים (10139)
    • תקציר הקורס:

    תקציר:

    שפות פורמליות, מכונות מצבים סופיות דטרמיניסטיות ולא דטרמיניסטיות,

     

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

     

    מכונות טיורינג ושפות כריעות וכריעות למחצה.
  • אימות תוכנה (10146)
    • תקציר הקורס:

    תקציר:

    הקורס מלמד את התאוריה ומתרגל את הפרקטיקה של הוכחות נכונות קוד בעזרת שימוש בשפה ובכלי (Dafny) שתומכים בפעילות זו על ידי אוטומציה חלקית של תהליך ההוכחה. במהלך הקורס הסטודנטים ילמדו בהדרגה תאוריה וטכניקות שיאפשרו להם לתאר דרישות נכונות ולהוכיח נכונות של תוכניות במורכבות הולכת וגדלה.
  • מידול מערכות תכנה (10148)
    • תקציר הקורס:

    תקציר:

    הקורס מחולק לשני חלקים. בחלק הראשון נלמד איך לתאר מערכות תגובתיות כמכונות מצבים (transition systems) ואיך לתאר תכונות בטיחות וחיות בעזרת נוסחאות בלוגיקה טמפורלית. נשתמש בכלי NuSMV כדי לבדוק באופן אוטומטי האם התכונות הרצויות מתקיימות. בחלק השני נלמד איך לתאר מערכות עתירות מידע בעזרת לוגיקה רלציונית ואיך לנסח תכונות מבניות (structural invariants) והתנהגותיות בעזרת הלוגיקה הרלציונית והכלי Alloy analyzer.
  • הנדסת מערכות עתירות תוכנה (61212)
    • תקציר הקורס:

    תקציר:

    הקורס מתחלק לשני חלקים. בחלק הראשון נתמקד בהבנת התכונות המבדלות של מערכות תוכנה ואיך הן משפיעות על המורכבות של פיתוח מערכות כאלה. בחלק השני נתמקד בתיאור הטכניקות שבעזרתן אפשר להתמודד עם הבעיות שהתכונות שחקרנו מעלות. את נושאי הקורס ילוו מקרי בוחן של מערכות תוכנה שההצלחה או הכישלון של הפיתוח שלהן מדגימים את העקרונות התאורטיים. הסטודנטים יתחלקו לקבוצות עבודה קטנות וכל קבוצה תקבל כמשימה לתחקר כמה ממקרי הבוחן ולהציג אותם לכיתה. הציון בקורס יתחלק 50% הצגת התחקירים ו-50% בחינה. ציון התחקיר יהיה קבוצתי ויתחלק לחצי ציון ההצגה וחצי ציון דוח התחקיר. הבחינה תכלול שאלות גם על החומר התאורטי וגם על מקרי הבוחן.