Course Syllabus

Course Information：

Year-Semester Course Number Course Name Phase Credits Hours Required/Elective Instructor Class Student NO. Withdraw Note

Spring Semester
Year 2024 332402 Computational Logic and Software Verification 1 3.0 3 ★ LIN,Jyun-Ao MPIS
MSIS 7 0 電資資安和創新資安合開

Year-Semester	Course Number	Course Name	Phase	Credits	Hours	Required/Elective	Instructor	Class	Student NO.	Withdraw	Note
Spring Semester Year 2024	332402	Computational Logic and Software Verification	1	3.0	3	★	LIN,Jyun-Ao	MPIS MSIS	7	0	電資資安和創新資安合開

Course Plan：

Instructor LIN,Jyun-Ao　Office Hours

Email jalin@ntut.edu.tw

Last Updated 2024-05-15 17:40:34

Course Objective 數理邏輯是理論計算機科學各領域重要的基礎。在本課程中，重點關注於數理邏輯在軟體程式驗證與機器可檢驗之證明等的應用。透過各種如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.

Course Schedule 1) Proportional Logic (4 weeks) 2) First-Order Logic and Satisfiability (4 weeks) 3) Model Checking (4 weeks) 4) Program Verification (4 weeks)

Evaluation and grading policy Homework 50% Mid-term 20% Final 20% Attendance 10%

Materials All right reserved. Do not reproduce without permission.

Foreign-language textbooks:No
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.

The access to curricular consultation Email: jalin@ntut.edu.tw

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

The course corresponds to the SDGs

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

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

Instructor	LIN,Jyun-Ao　Office Hours
Email	jalin@ntut.edu.tw
Last Updated	2024-05-15 17:40:34
Course Objective	數理邏輯是理論計算機科學各領域重要的基礎。在本課程中，重點關注於數理邏輯在軟體程式驗證與機器可檢驗之證明等的應用。透過各種如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.
Course Schedule	1) Proportional Logic (4 weeks) 2) First-Order Logic and Satisfiability (4 weeks) 3) Model Checking (4 weeks) 4) Program Verification (4 weeks)
Evaluation and grading policy	Homework 50% Mid-term 20% Final 20% Attendance 10%
Materials	All right reserved. Do not reproduce without permission. Foreign-language textbooks:No 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.
The access to curricular consultation	Email: jalin@ntut.edu.tw Week 17&18: Final Project Presentation (Online via course Teams)
The course corresponds to the SDGs
Note	課程網頁：https://carquois42.github.io/Logic.html Week 17&18: Final Project Presentation (Online via course Teams)