Sign In

לימודי שיטות פורמליות בתואר שני במדעי המחשב

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

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

 

המרצים בתחום

מרצים מסגל המחלקה:
 פרופ' אמיר בן-עמרם  ·  פרופ' שמואל טישברוביץ' · ד"ר שרון שוהם בוכבינדר

מרצים מן החוץ:
ד"ר רן אטינגר  ·  ד"ר דוד פייטלסון  ·  אורן איש שלום


רשימה אופייניית של קורסים לתואר שני בתחום*

עקרונות שפות תכנות  (מרצה: פרופ' אמיר בן-עמרם)

מבוא לאנליזה סטטית של תוכניות (מרצה: פרופ' אמיר בן-עמרם)

אימות אוטומטי של מערכות (מרצה: ד"ר שרון שוהם בוכבינדר)

הנדסת תוכנה (מרצה: פרופ' שמואל טישברוביץ')

טרנספורמציות לשיפור איכות קוד קיים (מרצה: ד"ר רן אטינגר)


סמינרים

סמינר באימות פורמלי של מערכות  (מרצה: ד"ר שרון שוהם בוכבינדר)


קורסי רקע

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

לוגיקה למדעי המחשב

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


קורסים שניתנו בשנים האחרונות כקורס בחירה משותף לתלמידי תואר שני וראשון

בניית תוכניות עם הוכחה (מרצה: ד"ר רן אטינגר)

מולטי-תכנות לעיבוד מקבילי (מרצה: ד"ר רן אטינגר)

ניתוח תוכנה מכוון מודלים (מרצה: דוד פייטלסון)

קומפיילרים וניתוח מתקדם של שפות תכנות (מרצה: אורן איש שלום)


קישורים להיכרות עם התחום

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

אוסף רחב של קישורים למחקר, כינוסים ועוד


עבודות גמר נבחרות

 Automatic Complexity Analysis of Simple Imperative Programs

ביצע: צחי מן

מנחה: פרופ' אמיר בן-עמרם

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

תוכנת הדגמה      מצגת על הפרויקט

Solving Range Constraints for Interval Analysis

ביצעה: שלומית אריאן

מנחים: פרופ' אמיר בן-עמרם, ד"ר איריס רוזנבלום

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

תקציר מורחב