課程說明
軟體工程中形式方法導論，涵蓋命題與一階邏輯（句法、語意、證明理論）、形式規格語言、有界分析與驗證、形式規格工具，以及以有限狀態機、時序邏輯與模型檢查工具進行之模型檢查。
先修條件
- 先修課程：COMP 1805、SYSC 3120 及 SYSC 4001 。
條件與方式
- 先修課程：COMP 1805、SYSC 3120 及 SYSC 4001 。
- 每週授課三小時。
原文參考文本
Introduction to formal methods in software engineering with coverage of propositional and first-order logic (syntax, semantics, proof theory), formal specification languages, bounded analysis and validation, formal specification tools, and model checking with finite-state machines, temporal logic, and model checking tools.
- Prerequisite(s): COMP 1805 , SYSC 3120 , and SYSC 4001 .
- Lectures three hours a week.
來源與參考
保留日期與來源以協助你核實資料。為便於閱讀提供譯文；官方來源為條件與要求的參照。
來源參考 : https://calendar.carleton.ca/undergrad/courses/SYSC/