Introduction

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

Announcements

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

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

（傳統）程式一定會有錯

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

（自動）推論幫你找到錯

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

（電腦）邏輯研究面面觀

除了自動驗證與測試，我們還會提到更多邏輯在電腦科學的研究議題。預計將以特別演講的方式呈現。

Important dates

  1. 05/31
    網站上線
  2. 07/13
    外校學生修課報名開始
  3. 07/14
    外校學生修課報名截止
  4. 07/19
    臺大學生報名開始
  5. 07/20
    臺大學生報名截止
  6. 07/24
    旁聽報名截止(07/31通知結果)
  7. 07/27
    課程網路加退選截止
  8. 08/21
    課程開始
  9. 08/28
    期中停修截止
  10. 09/01
    課程結束

Courses

Automata Theory

Taught by

Bow-Yaw Wang
Institue of Information Science
Academia Sinica

Resources

Handouts & Slides

Automated Decision Procedure for Propositional Logic

Taught by

Ming-Hsien Tsai
National Institute of Cyber Security

Resources

Handouts & Slides

Quantified Boolean Formula Satisfiability's Applications to Synthesis and Verification

Taught by

Jie-Hong Jiang
Department of Electrical Engineering
National Taiwan University

Resources

Handouts & Slides
Homework

Satisfiability Modulo Theories (SMT)

Taught by

Yu-Fang Chen
Institue of Information Science
Academia Sinica

Resources

Handouts & Slides
Example Codes

Basic Complexity Theory

Taught by

Tony Tan
University of Liverpool

Resources

Handouts & Slides

SMT-based Program Testing

Taught by

Fang Yu
Department of Management Information Systems
National Cheng Chi University

Resources

Handouts & Slides

Automata-based Parameterized Model Checking and Synthesis

Taught by

Chih-Duo Hong
Department of Management Information Systems
National Cheng Chi University

Resources

Handouts & Slides

Special Talk — Incorrectness Logic and Underapproximation: Foundations of Bug Catching

The talk would cover the discussion of incorrectness separation logic and its applications in industry (e.g., finding bugs in software development at Meta.)

Speaker

Lê Quang Lộc
Department of Computer Science
University College London

Slides

Download

Special Talk — Automatically Debugging AutoML Pipelines Using Maro: ML Automatted Remediaiton Oracle

The talk would focus on how to look for ways to improve AutoML search spaces via SMT. It also involves, effectively, using SMT to generate code.

Speaker

Julian Dolby
Thomas J.Watson Research Center
Yorktown Heights
NY USA

課表

1st week Mon Tue Wed Thu Fri
Morning 命題邏輯與其自動化決策程序Automated Decision Procedure for Propositional Logic 命題邏輯與其自動化決策程序Automated Decision Procedure for Propositional Logic 自動機理論Automata Theory QBF可滿足性與其在合成與驗證的應用Quantified Boolean Formula Satisfiability's Applications to Synthesis and Verification QBF可滿足性與其在合成與驗證的應用Quantified Boolean Formula Satisfiability's Applications to Synthesis and Verification
Afternoon 命題邏輯與其自動化決策程序Automated Decision Procedure for Propositional Logic 自動機理論Automata Theory 自動機理論Automata Theory QBF可滿足性與其在合成與驗證的應用Quantified Boolean Formula Satisfiability's Applications to Synthesis and Verification 基於自動機理論的可參數化模型驗證與合成Automata-based Parameterized Model Checking and Synthesis
2nd week Mon Tue Wed Thu Fri
Morning Satisfiability Modulo Theories (SMT)Satisfiability Modulo Theories (SMT) 演講1Incorrectness Logic and Underapproximation: Foundations of Bug Catching 基礎複雜度理論Basic Complexity Theory 演講2Automatically Debugging AutoML Pipelines Using Maro: ML Automatted Remediaiton Oracle 考試Exam
Afternoon Satisfiability Modulo Theories (SMT)Satisfiability Modulo Theories (SMT) Satisfiability Modulo Theories (SMT)Satisfiability Modulo Theories (SMT) 基礎複雜度理論Basic Complexity Theory 基於SMT的程式測試SMT-based Program Testing 討論與意見回饋 Discussion and Feedback