ברוכים הבאים לאתר הקורס: אימות בשיטות פורמאליות

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

שקפים:

ניתן להוריד את המצגות מההרצאות מהתיקיה "Class material"

אופן חישוב הציון:

במהלך הקורס ינתנו עבודות בית, יתקיים בוחן אמצע ומבחן מסכם. הציון יקבע באופן הבא: הציון הממוצע של העבודות ישוקלל כ-30% בציון הסופי, ציון הבוחן ישוקלל כ-25% בציון הסופי והמבחן הסופי ישוקלל כ-45% מהציון. כדי לעבור את הקורס חובה להגיש את כל עבודות הבית ולהשיג ציון גבוה מ-55 במבחן. אפשר להגיש את העבודות בזוגות.

חומר הקורס מתבסס על הספר:
Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press