ד"ר יוני זוהר

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

מחקרו מתמקד באימות פורמלי (Formal Verification) ובפרט בפותרני אילוצים (SMT Solvers) - אלגוריתמים הפותרים בעיות לוגיות ומתמטיות מורכבות בזמן קצר. עבודתו נעה בין לוגיקה מתמטית לבין יישומים מעשיים, ומשפיעה על הדרך שבה מערכות תוכנה נבדקות ומובטחות לפעול בצורה תקינה, גם בתנאים מורכבים.

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

• פותרני ספיקות עם תיאוריות רקע (SMT Solvers)

• לוגיקה מתמטית והסקה אוטומטית (Automated Reasoning)

• אימות פורמלי של תוכנה (Formal Verification)

• אימות חוזים חכמים (Smart Contract Verification)

אופי המחקר:

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

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

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

• תעשייה: פיתוח כלי אימות בחברות טכנולוגיה מובילות

• אקדמיה: חוקרים ומרצים בתחומי לוגיקה ואימות פורמלי

• יזמות: פיתוח כלים לאימות קוד AI וחוזים חכמים