הקורס מלמד את התאוריה ומתרגל את הפרקטיקה של הוכחות נכונות קוד בעזרת שימוש בשפה ובכלי (Dafny) שתומכים בפעילות זו על ידי אוטומציה חלקית של תהליך ההוכחה. במהלך הקורס הסטודנטים ילמדו בהדרגה תאוריה וטכניקות שיאפשרו להם לתאר דרישות נכונות ולהוכיח נכונות של תוכניות במורכבות הולכת וגדלה.
הקורס מחולק לשני חלקים. בחלק הראשון נלמד איך לתאר מערכות תגובתיות כמכונות מצבים (transition systems) ואיך לתאר תכונות בטיחות וחיות בעזרת נוסחאות בלוגיקה טמפורלית. נשתמש בכלי NuSMV כדי לבדוק באופן אוטומטי האם התכונות הרצויות מתקיימות. בחלק השני נלמד איך לתאר מערכות עתירות מידע בעזרת לוגיקה רלציונית ואיך לנסח תכונות מבניות (structural invariants) והתנהגותיות בעזרת הלוגיקה הרלציונית והכלי Alloy analyzer.
