לינור צוק
| לינור ד' צוק |
|---|
| שנת לידה: 1958 |
| ענף מדעי: מדעי המחשב, אימות תוכנה ופרטיות מידע |
| השכלה: הטכניון; תואר שני ודוקטורט ממכון ויצמן למדע |
| תרומות עיקריות: שיטות מתמטיות לבדיקת נכונותן של תוכנות, מהדרים ופרוטוקולי תקשורת |
פרסים והוקרה:
|
לינור ד' צוק (באנגלית: Lenore D. Zuck; נולדה ב-1958) היא מדענית מחשב ישראלית־אמריקאית ופרופסורית מחקר באוניברסיטת אילינוי בשיקגו. מחקרה עוסק בשיטות פורמליות להנדסת תוכנה — שימוש בלוגיקה ובכלים מתמטיים לבדיקת עמידתן של מערכות בדרישות שהוגדרו להן — וכן באבטחת מערכות ובפרטיות מידע.[1][2]
ביוגרפיה וקריירה
צוק נולדה בתל אביב בשנת 1958. היא קיבלה תואר ראשון מהטכניון ב-1979, תואר שני ממכון ויצמן למדע ב-1983 ודוקטורט במדעי המחשב ממכון ויצמן ב-1987.[3][4] עבודת הדוקטורט שלה, Past Temporal Logic, נכתבה בהנחיית אמיר פנואלי ועסקה בלוגיקה טמפורלית, המאפשרת לתאר כיצד תכונות של מערכת משתנות לאורך זמן.[5]
לאחר לימודיה הייתה חברת סגל במדעי המחשב באוניברסיטת ייל, ובהמשך עבדה באוניברסיטת ניו יורק. בראשית שנות ה-2000 הצטרפה לאוניברסיטת אילינוי בשיקגו.[6]
מחקר ותרומה מדעית
צוק חוקרת דרכים להוכיח שתוכנה פועלת כנדרש גם כאשר יש לה מצבים אפשריים רבים או אינסופיים. תחומי עבודתה כוללים הוכחת משפטים, בדיקת מודלים, הפשטה של מערכות וניתוח פורמלי של פרוטוקולי אבטחה. בפרסומיה המשותפים עם פנואלי ועם חוקרים נוספים עסקה גם בפרוטוקולים הסתברותיים ובמערכות מבוזרות, שבהן כמה רכיבים פועלים ומתקשרים זה עם זה.[1][4]
תחום מרכזי נוסף בעבודתה הוא תיקוף תרגום של תוכניות מחשב. מהדר ממיר תוכנית לצורה אחרת ומבצע לעיתים שינויים שנועדו לשפר את ביצועיה. תיקוף תרגום בוחן אם התוצאה של ההמרה המסוימת שומרת על התנהגות התוכנית המקורית. צוק ושותפיה פיתחו שיטות לתיקוף שינויים כאלה, לרבות שינויים בלולאות, וכן לבדיקת תאימות לאחור במיקרו־קוד — שכבת הוראות פנימית של המעבד. במחקר על מיקרו־קוד נבחנה האפשרות להבטיח שעיצוב חדש של מעבד ימשיך לתמוך בקוד הישן כאשר התכונות החדשות כבויות.[6][1]
מחקריה המאוחרים יותר כוללים שאלות של שיתוף מידע תוך שמירה על פרטיות. במסגרת מיזם שקיבל מימון ממכון Discovery Partners הובילה צוות לפיתוח פלטפורמה לאכיפת כללי פרטיות, בין היתר במערכות בריאות. מטרת העבודה הייתה גם לפתח כלים לבחירת האיזון בין הגנה על מידע אישי ובין התועלת שאפשר להפיק מנתונים.[2]
פרסומים נבחרים
- עם אורנה ליכטנשטיין ואמיר פנואלי: The Glory of the Past, 1985 — מחקר בלוגיקה טמפורלית.
- עם ג'וזף הלפרן: A Little Knowledge Goes a Long Way, Journal of the ACM, 1992 — גזירת פרוטוקולים והוכחת נכונותם באמצעות ייצוג ידע.
- עם אמיר פנואלי: Probabilistic Verification, Information and Computation, 1993.
- עם יהודה אפק, חגית עטיה ושותפים נוספים: Reliable Communication over Unreliable Channels, Journal of the ACM, 1994.
- עם ניקולס קריירו ודייוויד גלרנטר: Bauhaus Linda, 1995.
- עם אמיר פנואלי ו-Sitvanit Ruah: Automatic Deductive Verification with Invisible Invariants, 2001.
- עם אמיר פנואלי וג'סי שו: Liveness with (0, 1, ∞)-Counter Abstraction, 2002.
פרסים והוקרה
בשנת 2014 הוענק לצוק מעמד של חברה מצטיינת ב-ACM, האגודה הבין־לאומית למחשוב, במסגרת ההוקרה על תרומות מקצועיות ומדעיות בתחום המחשוב.[7]
קישורים חיצוניים
- לינור צוק באתר אוניברסיטת אילינוי בשיקגו (באנגלית)
- אתר הבית של לינור צוק (באנגלית)
הערות שוליים
- ↑ 1.0 1.1 1.2 Lenore Zuck, המחלקה למדעי המחשב, אוניברסיטת אילינוי בשיקגו (באנגלית).
- ↑ 2.0 2.1 UIC Faculty Members Earn DPI Funding — Lenore Zuck, לשכת סגן הנשיא למחקר, אוניברסיטת אילינוי בשיקגו (באנגלית).
- ↑ Verification of Multiprocess Probabilistic Protocols, אמיר פנואלי ולינור צוק, Distributed Computing, כרך 1, 1986, עמ' 53–72; פסקת הביוגרפיה של המחברת.
- ↑ 4.0 4.1 Graduate Handbook: Faculty — Lenore Zuck, המחלקה למדעי המחשב, אוניברסיטת ייל (באנגלית).
- ↑ Lenore D. Zuck, פרויקט הגנאלוגיה המתמטית (באנגלית).
- ↑ 6.0 6.1 Lenore Zuck: Microcode Verification, אוניברסיטת קרנגי מלון, 21 באוקטובר 2005 (באנגלית).
- ↑ ACM's Distinguished Computer Scientists, Engineers and Educators Cited for Global Reach, Real-World Impact, ACM, 4 בדצמבר 2014 (באנגלית).