עיתון אוניברסיטת בן-גוריון בנגב
הוכחה להצלחה
קבלו טיפ תלמדו לנצל את התקופות הרגועות יותר לטובת המשפחה, וכך חוסר האיזון בתקופות הלחוצות יותר יהיה פחות קשה
מושג ההוכחה מוכר לכולנו מן העולם המתמטי, אך גם במדעי המחשב יש לו חשיבות עצומה. בעולם המודרני שבו הטכנולוגיה שולטת בכל רובדי החיים, הכרחי לוודא שמערכות ממוחשבות אכן מבצעות את מה שהן אמורות לבצע. ד"ר לירון כהן, חברת סגל המחלקה למדעי המחשב, שִכללה את הפיקוח על אותן מערכות, ובמסגרת מחקרה היא שואפת ד"ר לירון כהן, חברת סגל המחלקה למדעי המחשב, חוקרת דרכים לשיפור הפיקוח על מערכות ממוחשבות כדי לוודא שהן פועלות במסגרת מחקרה היא מפתחת | ללא דופי רעיונות ומושגים מודרניים של חישוביות והוכחה
אחת הדרכים האמינות והיעילות ביותר להבטיח התנהגות מסוימת של תוכנה, מעבר לכל צל של ספק, היא על ידי כתיבת הוכחה פורמלית. כלומר, נרצה להוכיח באופן פורמלי שהתנהגות מסוימת, כגון הימנעות מפגיעה בהולכי רגל, תתקיים בכל מצב אפשרי של המערכת, קרי בכל נסיעה ברכב. אולם, כתיבת הוכחות היא מטלה לא פשוטה, במיוחד כאשר מדובר על הוכחות פורמליות שבהן כל פרט בהוכחה צריך להיות מנומק. מטרתה של ד"ר כהן היא לפתח רעיונות ומושגים מודרניים של חישוביות והוכחה ולשלבם במערכות שעליהן מושתתים עזרי ההוכחה. לשם כך היא משלבת חידושים מתחומי מחקר שונים, כגון תורת ההוכחה, שפות פורמליות ותורת
להגביר את יכולותיהן על-ידי הרחבת היסודות החישוביים העומדים בבסיסם. נשמע מסובך? הביצוע עוד יותר מורכב. החידושים הטכנולוגיים לא נעצרים לרגע והם משפיעים על מסלולי חיינו. למשל: לפני שניכנס לרכב אוטונומי נרצה להיות בטוחים שתוכנית המחשב ששולטת בו אכן נמנעת מפגיעה בהולכי רגל; ולפני שניכנס לניתוח נרצה להיות משוכנעים שהמכשור הרפואי המתקדם המותקן בחדר הניתוחים מבצע את מטרתו כהלכה. תהליך זה קרוי אימות.
מדע וטכנולוגיה | 10
Made with FlippingBook Annual report maker