פרופ' דורון פלד

שיטות פורמליות, אמינות תוכנה ובינה מלאכותית

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

תחומי מחקר מרכזיים:

• שיטות פורמליות (Formal Methods)

• בדיקת מודלים (Model Checking)

• אימות בזמן ריצה (Runtime Verification)

• אמינות AI ו-LLM

אופי המחקר:  

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

אופק תעסוקתי:

בוגרות ובוגרי המעבדה משתלבים במגוון תפקידים:

• תעשייה: מהנדסי אמינות תוכנה ומומחי אימות במערכות קריטיות – תעופה, רפואה, רכב אוטונומי

• אקדמיה: חוקרים ומרצים בתחומי שיטות פורמליות ואבטחת תוכנה

• הייטק: מפתחי כלים לאימות קוד המיוצר על ידי AI בחברות טכנולוגיה מובילות