תקציר הקורס (להרחבה)

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

מטרות/תוצרי הלמידה (להרחבה)

1. הלומדים יקודדו בעיות מתחומים שונים כבעיות ספיקות ויפעילו פותרנים מתאימים כדי לפתור אותן.
2. הלומדים יתארו ויממשו אלגוריתמים לפתרון בעיות ספיקות שונות.
3. הלומדים יוכיחו שהאלגוריתמים המצוינים לעיל נכונים.

 למידה פעילה - תכנון מהלך השיעורים: (להרחבה)

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

ידע
1.
2.
3.

מיומנויות
1.
2.

ערכים (במידה ולא רלוונטי ניתן למחוק)
1.
2.

** ייתכנו שינויים בסילבוס בהתאם לקצב ההתקדמות ואפקטיביות הלמידה

מבחן ומטלות.

Decision Procedures: An Algorithmic Point of View by Kroening and Strichman

The Calculus of Computation by Bradley and Manna

חומרים נוספים יימסרו לפי הצורך.