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