ד"ר הדר פרנקל

אימות אוטומטי, לוגיקה טמפורלית ושפות פורמליות

במערכות קריטיות כמו מכונית אוטונומית, תשתיות ענן או אבטחת מידע רגיש, לכל באג קטן עלולות להיות השלכות על חיי אדם או נזק בלתי הפיך. בדיקות תוכנה סטנדרטיות (QA) בודקות רק את התרחישים שחשבנו עליהם מראש, אך במערכות מורכבות, מספר התרחישים האפשריים הוא עצום ובלתי ניתן  לכיסוי ידני. מחקרה של ד"ר פרנקל נועד להבטיח שלא יהיו טעויות; היא עושה זאת באמצעות אימות פורמלי - שימוש בכלים מתמטיים להוכחה שהתכנית עומדת בהגדרות שלה, ללא תלות בתרחיש הספציפי שחשבנו עליו. מעבר להוכחה, ד"ר פרנקל מפתחת שיטות על מנת  להסביר את הגורם לתקלות ואף להציע תיקון אוטומטי (Program Repair) למערכת. 

עקרונות אלה מיושמים כיום להבטחת אמינות בשבבים מורכבים ובמערכות קריטיות רבות.

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

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

• אבטחה ופרטיות: אימות תכונות מורכבות (Hyperproperties) המבטיחות למשל שמידע רגיש לא ידלוף, ומאפשרות לדבר בצורה פורמלית על הוגנות, סיבתיות, ועוד. 

• סיבתיות  וניתוח התנהגות של תכניות: פיתוח כלים המאפשרים להסביר בצורה אוטומטית כשלים או התנהגויות של תכניות. 

אופן המחקר:

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

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

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