Introduction

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

Announcements

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

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

(傳統)程式一定會有錯

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

(自動)推論幫你找到錯

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

(電腦)邏輯研究面面觀

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

Important dates

  1. 6/1
    宣佈停辦

Courses

命題邏輯與一階邏輯

Taught by

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

驗證密碼學程式

Taught by

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

霍爾邏輯

Taught by

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

邏輯的理論研究

Taught by

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

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

Taught by

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

布林可滿足性演算法

Taught by

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

程式驗證導論/SMT 演算法

Taught by

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

Dafny 程式驗證工具

Taught by

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

基於 SMT 的程式測試

Taught by

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

Special Talk — Introduction to Static Data-flow Analysis

Speaker

Max Schäfer
GitHub, Inc.