邏輯、語言與計算暑期研習營
Formosan Summer School on Logic, Language, and Computation, 20258/11-8/22 09:10-12:10, 13:20–16:20
地點：國立臺灣大學電機二館229教室
Formosan Summer School on Logic, Language, and Computation, 2025近年來，從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識；然而，國內從事此類研究的學者分散在各校，難以僅靠一己之力開設整套課程。因此，我們邀請有相同興趣的學者一同開課，訓練下一代的研究人才。 邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從2008年起，本研習營在兩大主題之間輪流替換。今年之主題為邏輯與正規驗證。 自 2012 年起，本研習營正式成為台灣大學暑修課程，針對大學部學生開課，但亦歡迎研究生選修。台灣大學學生可透過國立台灣大學暑期課程網選課，有學籍之其他學校學生可透過校際選修選課。 邏輯、語言與計算」暑期研習營從2007年開始至今每年舉辦，今年為第十九屆。
待公布
命題邏輯是最基礎的形式邏輯系統，以「命題」──可判定真假的敘述──為最基礎的建構單元，透過 AND、OR、NOT、IMPLIES 等連接詞組合出複雜公式。它提供了真值表與演繹規則，讓我們能以機械化方式判斷公式的有效性，並為證明、程式驗證與自動定理證明奠定核心工具。透過學習命題邏輯，學生將掌握形式化推理的語法與語義，為後續的述詞邏輯、型別理論與 SMT 技術建立扎實基礎。
SAT（布林可滿足性問題）與二元決策圖（Binary Decision Diagram, BDD）是現代邏輯優化與自動化推理的兩大支柱。SAT 透過高效求解器判定布林公式是否存在滿足解，已成為硬體驗證、形式化檢查與組合最佳化的核心工具；BDD 則以圖形化結構將布林函式壓縮為共享決策樹，使得等價判定與函式操作在圖上即可快速進行。本課程將介紹 SAT 演算法（DPLL、CDCL）、BDD 建構與簡約技巧，並展示二者在電路設計、軟體分析及 AI 規劃中的互補應用，讓學員習得在實務系統中選擇與整合這兩種技術的關鍵思維。
硬體模型檢查（Hardware Model Checking）是一種自動化形式化驗證技術，透過在狀態空間中系統性地探索電路模型，確保晶片設計滿足時間邏輯（如 LTL／CTL）所描述的安全與活性性質。課程將聚焦於符號式模型檢查（BDD 與 SAT/SMT-based）、邊界模型檢查（BMC）、及形式財產驗證（FPV）的實務流程，並示範如何將 Verilog/VHDL 轉換為過渡系統、撰寫屬性、解析失敗範例（counter-example），以及運用工業級工具在 SoC 及 FPGA 專案中提早捕捉設計缺陷，縮短迴圈、提升可靠度。
一階邏輯（First-order Logic, FOL）在命題邏輯的基礎上加入「變數、量詞與謂詞」，能精確表達「所有…皆…」與「存在…使…」等結構化敘述，是數學證明、程式規格與自動定理證明的核心語言。本課程將介紹 FOL 的語法與語意、自由與束縛變數、模型與滿足關係，以及完備性與可靠性等基本定理；進一步探討一階合取標準形、分辨率（resolution）演算法及其在 SMT 解題、軟體驗證和資料庫查詢中的應用，讓學員奠定形式化推理與邏輯推導的堅實基礎。
SMT（Satisfiability Modulo Theories，模組理論可滿足性）將 SAT 的布林求解核心與多種理論（如整數/實數算術、位向量、陣列、字串、遞歸資料結構等）結合，能直接處理帶有數學運算與資料結構的約束。現代 SMT 求解器採用 DPLL(T) 框架，協調 SAT 引擎與專用理論決策程序，已成為軟體/硬體驗證、符號執行、自動合成與優化領域的關鍵基礎。本課程將介紹 SMT-LIB 語法、DPLL(T) 演算法、主流理論決策器的原理，並透過實例展示如何在程式分析、模型檢查與約束優化中高效運用 SMT 技術。
自動機理論是理論計算機科學的基石，研究有限狀態機、推疊自動機、圖靈機等抽象運算模型，以及它們所辨識的形式語言階層（正則語言、上下文無關語言等）。藉由描述狀態轉移與接受條件，自動機為編譯器、正則表示式引擎、模型檢查乃至自然語言處理提供精確的規格與分析工具。本課程將介紹正則運算、DFA/NFA 等價轉換、PDA 與 CFG 的對應、決定性與不可決定性、語言封閉性與可判定性等核心概念，並透過實作展示自動機在程式語言分析與模式比對中的實務應用。
軟體模型檢查（Software Model Checking）以自動化技術在程式的狀態空間中探索，驗證其是否滿足安全與活性等規格。相較於傳統測試，它能覆蓋所有可達路徑並於發現錯誤時給出具體反例。課程將介紹抽象解釋與 CEGAR（Counter-Example Guided Abstraction Refinement）、符號與路徑取樣方法（如 Bounded Model Checking、符號執行）、以及現代工具（BLAST、CPAchecker、SPIN、KLEE）的核心演算法與實務工作流程。透過案例研究，學員將學會如何把 C/C++、Java、Rust 程式轉換成可驗證模型、撰寫屬性、分析反例，並將模型檢查整合進 CI/CD 以在開發早期捕捉潛在缺陷。
本課程聚焦於 自動機學習（Automata Learning），特別是 Angluin 經典的 L* 主動學習演算法，並介紹其在 參數化驗證 中的創新應用。L* 透過「查詢–反例」迴圈自動推導最小 DFA，為未知或黑箱系統建構可機械分析的模型。當系統包含任意數量的相同元件時，我們結合學到的自動機與抽象加強技術，形成一般化不變式並保證性質對所有規模都成立。
本課程將介紹如何運用 「有限／符號自動機」來建模程式中的字串與輸入資料流，並自動偵測與修補常見漏洞（如 XSS、SQL 注入）。內容源自郁方教授在自動機式字串分析工具 STRANGER 與「前向／回溯符號分析產生漏洞簽章」等研究成果，說明自動機模型如何結合 SMT 求解器與查詢-反例迴圈，精準判定安全屬性並生成防護簽章。
量化可滿足性（Quantified Satisfiability，QBF）在布林 SAT 上加入全稱與存在量詞，可自然編碼控制器合成、時序邏輯驗證等 PSPACE 完備問題。現代 QBF 求解器支援 Skolem／Herbrand 函式擷取，使「公式為真」時立即產生實作策略，「公式為假」則提供可解析的反例。課程將介紹 prenex-CNF 編碼、DPLL(Q) 與 expansion 求解，以及 QBF 證書在合成與錯誤診斷中的實務應用。
待公布
| 第一週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | 命題邏輯 | 硬體模型檢測 | 一階邏輯 | 模組理論可滿足性 | 自動機理論 |
| 下午 | 布林可滿足性問題與二元決策圖 | 硬體模型檢測 | 一階邏輯 | 模組理論可滿足性 | 自動機理論 |
| 第二週 | 星期一 | 星期二 | 星期三 | 星期四 | 星期五 |
|---|---|---|---|---|---|
| 上午 | 軟體模型檢測 | 自動機學習與參數化驗証 | 自動機與軟體安全 | 量化可滿足性及其在合成與驗證中的應用 | 期末考式Exam |
| 下午 | 軟體模型檢測 | 自動機學習與參數化驗証 | 自動機與軟體安全 | 量化可滿足性及其在合成與驗證中的應用 | 邀請講座SMT over String theory |