פורטל הסטודנטים

הקורס יילמד בשני פרקים עיקריים: 1. היסק אוטומטי - שיטות וכלים בתחומי הוכחה פורמלית של תכונות של תכניות מחשב וסמנטיקה פורמלית של שפות תכנות. הנושאים יכללו: תחשיב למבדא, טיפוסים, פולימורפיזם, TYPE THEORY, הצרנת סמנטיקה בלוגיקה מסדר ראשון, SATISFIABILITY MODULO THEORY. 2. סינתזה של תוכנה - ייצור אוטומטי של קוד על-ידי מהדר. הנושאים יכללו: SYNTAX-GUIDED SYNTHESIS, תכנות על פי דוגמאות, COUNTEREXAMPLE-GUIDED INDUCTIVE SYNTHESIS,. TYPE-DIRECTED AND DEDUCTIVE SYNTHESIS תוצאות למידה: בסיום הקורס, הסטודנטים: 1. יבינו את הבניה של הוכחות בלוגיקה פורמלית מתוך עקרונות מתמטיים יסודיים, ואת ההבדלים בין הוכחות פורמליות לבין הוכחות רגילות עם דף ועט. 2. יכירו את המושגים לוגיקה קונסטרוקטיבית ו-MARTIN-LOEF TYPE THEORY, בדגש על ההבדלים בינה לבין לוגיקה קלאסית ועל המתאם הוכחות-תכניות._ 3. יפתחו מיומנות הוכחת טענות באמצעות COQ PROOF ASSISTANT, מערכת להצרנה מכנית של הוכחות המבוססת על DEPENDENT TYPES. 4. ילמדו על הצרנה של תכונות המתייחסות לתכניות מחשב, באמצעות שני סוגים מקובלים של סמנטיקה פורמלית: סמנטיקה ביצועית וסמנטיקה אקסיומטית, ולהוכיח תכונות אלו הן בעזרת COQ והן בהתבסס על הוכחה אוטומטית תוך שימוש בכלי SMT. 5. ידעו לסווג את הגישות השונות לסינתזה של תוכנה, ויכירו דוגמאות של אלגוריתמים המיישמים כל אחת מן הגישות הללו. 6. יתנסו בסינתזה של תכניות בעזרת כלי סינתזה: SKETCH ו-SYNQUID. 7. יפתחו בעצמם כלי סינתזה של תוכנה, בהתבסס על אלגוריתמים ואופטימיזציות שנלמדו, במסגרת פרויקט מסכם.

פקולטה: מדעי המחשב
|תואר ראשון |תארים מתקדמים

מקצועות צמודים

236360 - תורת הקומפילציה