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