查詢教學大綱與進度

教學大綱與進度

課程基本資料：

學年期課號課程名稱階段學分時數修教師班級人撤備註

112-2 332402 計算邏輯與軟體驗證 1 3.0 3 ★ 林濬璈資訊安全學位學程
創新資安學位學程 7 0 電資資安和創新資安合開

學年期	課號	課程名稱	階段	學分	時數	修	教師	班級	人	撤	備註
112-2	332402	計算邏輯與軟體驗證	1	3.0	3	★	林濬璈	資訊安全學位學程創新資安學位學程	7	0	電資資安和創新資安合開

教學大綱與進度：

教師姓名林濬璈　教師諮商時間(Office Hours)

Email jalin@ntut.edu.tw

最後更新時間 2024-05-15 17:40:34

課程大綱數理邏輯是理論計算機科學各領域重要的基礎。在本課程中，重點關注於數理邏輯在軟體程式驗證與機器可檢驗之證明等的應用。透過各種如SAT/SMT求解器與輔助證明工具Coq等，本課程將涵蓋以下主題：比例邏輯、一階邏輯、可滿足性模組理論、模型檢查與程式驗證。 Mathematical logic is an important foundation of various fields in theoretical computer science. This course focuses on its applications from software/program verification to machine-checkable proofs. Through various tools like SAT/SMT solvers and proof-assistant Coq, this course will cover the following topics: proportional logic, first-order logic, satisfiability module theory, model checking and program verification.

課程進度 1) Proportional Logic (4 weeks) 2) First-Order Logic and Satisfiability (4 weeks) 3) Model Checking (4 weeks) 4) Program Verification (4 weeks)

評量方式與標準 Homework 50% Mid-term 20% Final 20% Attendance 10%

使用教材、參考書目或其他 【遵守智慧財產權觀念，請使用正版教科書，不得使用非法影印教科書】

使用外文原文書：否
This course does not have a required text book. We will be covering different topics, all of which, cannot be found in one book to recommend as a unique text book. Here is a list of books that will help you understand the course material: 1. Michael Huth, Mark Ryan. “Logic in Computer Science: Modelling and Reasoning about Systems.” 2nd Edition, Cambridge University Press. 2. Flemming Nielson, Hanne Riis Nielson, Chris Hankin. “Principles of Program Analysis.” Springer. 3. Christel Baier, Joost-Pieter Katoen. “Principles of Model Checking.” MIT Press. 4. Aaron R. Bradley, Zohar Manna. “The Calculus of Computation: Decision Procedures with Applications to Verification.” Springer. 5. Daniel Kroening, Ofer Strichman. “Decision Procedures: An Algorithmic Point of View.” Springer.

課程諮詢管道 Email: jalin@ntut.edu.tw

Week 17&18: Final Project Presentation (Online via course Teams)

課程對應SDGs指標

備註
課程網頁：https://carquois42.github.io/Logic.html

Week 17&18: Final Project Presentation (Online via course Teams)

教師姓名	林濬璈　教師諮商時間(Office Hours)
Email	jalin@ntut.edu.tw
最後更新時間	2024-05-15 17:40:34
課程大綱	數理邏輯是理論計算機科學各領域重要的基礎。在本課程中，重點關注於數理邏輯在軟體程式驗證與機器可檢驗之證明等的應用。透過各種如SAT/SMT求解器與輔助證明工具Coq等，本課程將涵蓋以下主題：比例邏輯、一階邏輯、可滿足性模組理論、模型檢查與程式驗證。 Mathematical logic is an important foundation of various fields in theoretical computer science. This course focuses on its applications from software/program verification to machine-checkable proofs. Through various tools like SAT/SMT solvers and proof-assistant Coq, this course will cover the following topics: proportional logic, first-order logic, satisfiability module theory, model checking and program verification.
課程進度	1) Proportional Logic (4 weeks) 2) First-Order Logic and Satisfiability (4 weeks) 3) Model Checking (4 weeks) 4) Program Verification (4 weeks)
評量方式與標準	Homework 50% Mid-term 20% Final 20% Attendance 10%
使用教材、參考書目或其他	【遵守智慧財產權觀念，請使用正版教科書，不得使用非法影印教科書】使用外文原文書：否 This course does not have a required text book. We will be covering different topics, all of which, cannot be found in one book to recommend as a unique text book. Here is a list of books that will help you understand the course material: 1. Michael Huth, Mark Ryan. “Logic in Computer Science: Modelling and Reasoning about Systems.” 2nd Edition, Cambridge University Press. 2. Flemming Nielson, Hanne Riis Nielson, Chris Hankin. “Principles of Program Analysis.” Springer. 3. Christel Baier, Joost-Pieter Katoen. “Principles of Model Checking.” MIT Press. 4. Aaron R. Bradley, Zohar Manna. “The Calculus of Computation: Decision Procedures with Applications to Verification.” Springer. 5. Daniel Kroening, Ofer Strichman. “Decision Procedures: An Algorithmic Point of View.” Springer.
課程諮詢管道	Email: jalin@ntut.edu.tw Week 17&18: Final Project Presentation (Online via course Teams)
課程對應SDGs指標
備註	課程網頁：https://carquois42.github.io/Logic.html Week 17&18: Final Project Presentation (Online via course Teams)