Course Syllabus

Course Information：

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

Spring Semester
Year 2025 343370 Computational Logic and Software Verification 1 3.0 3 ★ LIN,Jyun-Ao MSIS 9 0 　

Year-Semester	Course Number	Course Name	Phase	Credits	Hours	Required/Elective	Instructor	Class	Student NO.	Withdraw	Note
Spring Semester Year 2025	343370	Computational Logic and Software Verification	1	3.0	3	★	LIN,Jyun-Ao	MSIS	9	0

Course Plan：

Instructor LIN,Jyun-Ao　Office Hours

Email jalin@ntut.edu.tw

Last Updated 2024-12-22 17:56:15

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) SMT-based Model Checking (4 weeks) 4) Program Verification (4 weeks) Final presentation (2 weeks)

Evaluation and grading policy Homework 40% Mid-term 30% Final project 30%

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. [CC] Aaron R. Bradley, Zohar Manna. “The Calculus of Computation: Decision Procedures with Applications to Verification.” Springer. 5. [DP] Daniel Kroening, Ofer Strichman. “Decision Procedures: An Algorithmic Point of View.” Springer.

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

The course corresponds to the SDGs SDG4：優質教育（Quality Education）
SDG5：性別平等（Gender Equality）
SDG9：產業創新與基礎設施（Industry, Innovation and Infrastructure）

Note
課程網頁：TBA

Instructor	LIN,Jyun-Ao　Office Hours
Email	jalin@ntut.edu.tw
Last Updated	2024-12-22 17:56:15
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) SMT-based Model Checking (4 weeks) 4) Program Verification (4 weeks) Final presentation (2 weeks)
Evaluation and grading policy	Homework 40% Mid-term 30% Final project 30%
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. [CC] Aaron R. Bradley, Zohar Manna. “The Calculus of Computation: Decision Procedures with Applications to Verification.” Springer. 5. [DP] Daniel Kroening, Ofer Strichman. “Decision Procedures: An Algorithmic Point of View.” Springer.
The access to curricular consultation	Email: jalin@ntut.edu.tw
The course corresponds to the SDGs	SDG4：優質教育（Quality Education） SDG5：性別平等（Gender Equality） SDG9：產業創新與基礎設施（Industry, Innovation and Infrastructure）
Note	課程網頁：TBA