נקודות זכות באוניברסיטה העברית: 2

תואר: מוסמך

היחידה האקדמית שאחראית על הקורס: מדעי המחשב

סמסטר: סמסטר א'

שפת ההוראה: אנגלית ועברית

קמפוס: קרית א"י ספרא

מורה אחראי על הקורס (רכז): גיא כץ

דוא"ל של המורה האחראי על הקורס: guykatz@cs.huji.acil

שעות קבלה של רכז הקורס: בתאום מראש

מורי הקורס:
ד"ר גיא כץ

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

נתמקד ב: פתרנים לספיקות בוליאנית (SAT), פתרנים לספיקות מודולו תאוריות (SMT), ופתרני תכנות לינארי (LP)

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

מטרות הקורס:
לחשוף סטודנטים לאתגר, לאלגוריתמים, לשיטות ולכלים בחזית הטכנולוגיה לניתוח תוכנה, ולהציג בפניהם כמה מהבעיות הפתוחות בתחום

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

דרישות נוכחות (%):
הנוכחות חובה

שיטת ההוראה בקורס: הרצאות מקוונות סינכרוניות

רשימת נושאים / תכנית הלימודים בקורס:
פתרני SAT, פתרני SMT, פתרני LP, דדוקציה, הרצות סימבוליות, בדיקות מודל, אימות של רשתות נוירונים

חומר חובה לקריאה:
-

חומר לקריאה נוספת:

מרכיבי הציון הסופי :

מידע נוסף / הערות:
לתשומת לבכם, ייתכן והקורס יילמד בשפה האנגלית