課程介紹

近年來,從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識;然而,國內從事此類研究的學者分散在各校,難以僅靠一己之力開設整套課程。因此,我們邀請有相同興趣的學者一同開課,訓練下一代的研究人才。 邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從2008年起,本研習營在兩大主題之間輪流替換。今年之主題為邏輯與正規驗證。 自 2012 年起,本研習營正式成為台灣大學暑修課程,針對大學部學生開課,但亦歡迎研究生選修。台灣大學學生可透過國立台灣大學暑期課程網選課,有學籍之其他學校學生可透過校際選修選課。 邏輯、語言與計算」暑期研習營從2007年開始至今每年舉辦,今年為第十五屆。

公告事項

基於邏輯的程式測試與驗證

透過這次教學,我們希望讓大家了解邏輯對於寫程式的幫助。
現在基於邏輯的程式驗證與測試已經不僅僅是理論。許多大公司,已經積極地採用。 再不學,就來不及囉。
本次課程集結了國內相關研究的黃金陣容,講師來自中央研究院,台灣大學,政治大學。 無論經驗或是研究成果都是目前首選,相信不會讓大家失望。

(傳統)程式一定會有錯

現今程式的規模已經日益龐大,在實務上,以傳統方式開發的程式,只要超過一定的大小,無可避免的,一定或多或少會有一些錯誤。 這些錯誤,可大可小,常常會造成經濟上的損失或是更大的危害。

(自動)推論幫你找到錯

我們會討論各種基於邏輯的方法,自動化的幫忙找到程式錯誤,甚至證明修改過的已經完全符合定出來的規格。這些方法許多已經在最先進的業界被採用,有許多更前沿的方法還在學界開發中。

(電腦)邏輯研究面面觀

除了自動驗證與測試,我們還會提到更多邏輯在電腦科學的研究議題。範圍從理論到實務,在理論研究上,我們有多名講師有電腦邏輯最重要會議 LICS (Logic in Computer Science) 議程委員的經驗,在實務上,我們也有多位講師曾經或現在任職於頂尖軟體公司,處理相關工作,如硬體的 Cadence 和軟體的 GitHub。

重要日期

  1. 6/1
    宣佈停辦

課程

命題邏輯與一階邏輯

講師

王柏堯
中央研究院資訊科學研究所

驗證密碼學程式

講師

蔡明憲
中央研究院資訊科學研究所

霍爾邏輯

講師

穆信成
中央研究院資訊科學研究所
國立臺灣大學資訊管理學系

邏輯的理論研究

講師

陳偉松
國立臺灣大學資訊工程學系

布林可滿足性與其在合成與驗證的應用

講師

江介宏
國立臺灣大學電機工程學系

布林可滿足性演算法

講師

黃鍾揚
國立臺灣大學電機工程學系

程式驗證導論/SMT 演算法

講師

陳郁方
中央研究院資訊科學研究所

Dafny 程式驗證工具

講師

林子期
中央研究院資訊科學研究所

基於 SMT 的程式測試

講師

郁方
國立政治大學資訊管理學系

特別演講 — 資料流分析導論

主講人

謝邁思
GitHub, Inc.

課表

第一週 星期一 星期二 星期三 星期四 星期五
上午 程式驗證導論Introduction 命題邏輯與一階邏輯Propositional Logic and First Order Logic 霍爾邏輯Hoare Logic 布林可滿足性演算法Boolean Satisfiability Algorithms 布林可滿足性演算法Boolean Satisfiability Algorithms
下午 命題邏輯與一階邏輯Propositional Logic and First Order Logic 命題邏輯與一階邏輯Propositional Logic and First Order Logic 霍爾邏輯Hoare Logic 布林可滿足性求解器實習課TA session on SAT solvers SMT 演算法SMT Algorithms
第二週 星期一 星期二 星期三 星期四 星期五
上午 SMT 演算法SMT Algorithms 布林可滿足性問題在合成與驗證的應用Boolean Satisfiability’s Applications to Synthesis and Verification 邏輯的理論研究Theoretical Aspect of Logic Research 基於 SMT 的程式測試SMT-based Program Testing 考試Exam
下午 Dafny 程式驗證工具Dafny Program Verifier 布林可滿足性問題在合成與驗證的應用Boolean Satisfiability’s Applications to Synthesis and Verification 邏輯的理論研究Theoretical Aspect of Logic Research 驗證密碼學程式Crypto Program Verification 特別演講:資料流分析導論Introduction to static data-flow analysis