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