start

(2019/8/30) 今日下午的演講題目為“Java Program Verification Using Horn Clause” by Philipp Rümmer (Uppsala University)
(2019/8/29) Blockchain and Smart Contract Verification講義下載 slides
(2019/8/27) 8/29(四)的課程需要實作，請同學先至 link 下載並安裝。
(2019/8/27) 「課程內容」提供部分上課講義的下載連結 [持續更新]。
(2019/8/1) 旁聽報名繼續開放中。
(2019/8/1) 修課名單(~7/19報名)以及旁聽名單(~7/31報名)已經確定，已經寄送email通知。

近年來，從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識；然而，國內從事此類研究的學者分散在各校，難以僅靠一己之力開設整套課程。因此，我們邀請有相同興趣的學者一同開課，訓練下一代的研究人才。

「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從2008年起，本研習營在兩大主題之間輪流替換。今年之主題為邏輯與正規驗證。

自 2012 年起，本研習營正式成為台灣大學暑修課程，針對大學部學生開課，但亦歡迎研究生選修。台灣大學學生可透過國立台灣大學暑期課程網選課，有學籍之其他學校學生可透過校際選修選課。

「邏輯、語言與計算」暑期研習營從2007年開始至今每年舉辦，今年為第十三屆。

日期：2019 年 8 月 19 日 (週一) 至 8 月 30 日 (週五)，共計十天。

時間：每週一至週五早上九點至下午五點。

地點：台灣大學管理學院1號館102。

課程內容：

Propositional Logic (Bow-Yaw Wang) slides
First-Order Logic (Yu-Fang Chen) slides
Automata Theory (Ming-Hsien Tsai) slides
Description Logics and its Applications in AI and Knowledge Systems (Tony Tan)
Efficient decision procedure for propositional logic (SAT) (Andrea Turrini)
Boolean Satisfiability and Its Applications to Synthesis and Verification (QBF) (Roland Jiang) slides
Satisfiability Modulo Theories (SMT) (Hsin-Hung Lin) slides
Blockchain and Smart Contract Verification (Jun Furuse)Link to the slides
Automata-based String Manipulating Program Analysis (Fang Yu)slides1 slides2
Invited talk: Strings & Software Model Checking (Philipp Rümmer)slides

課程講者：

時間表 (暫定)：

時間	8/19 (一)	8/20 (二)	8/21 (三)	8/22 (四)	8/23 (五)
09:00~12:00	Propositional Logic	First-Order Logic	Description Logic	SAT	QBF
12:00~14:00	Lunch
14:00~17:00	Propositional Logic	First-Order Logic	Description Logic	SAT	QBF

時間	8/26 (一)	8/27 (二)	8/28 (三)	8/29 (四)	8/30 (五)
09:00~12:00	SMT	Automata	String	Blockchain	Final Exam
12:00~14:00	Lunch
14:00~17:00	SMT	Automata	String	Blockchain	Invited Talks

台大學生：

請於 07/19 (五)前線上填寫報名表。(報名已截止)
- 修課名單由主辦單位逕送教務處，學生無需線上選課。(已發e-mail通知)
- 報名超額時，將依所填之修課理由篩選。
繳費日期：08/16 ~ 08/20。

非台大學生：

旁聽報名

作業（40%）、期末考（60%）

最新消息