計算邏輯與軟體驗證

臺北科技大學 114-2 學期課程，課號 357455。

課程大綱

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

課程進度

The tentative schedule will cover 1) Program logics: reasoning principles for high-assurance software (9-10 weeks) - the birth of program logics - Haore logic - separation logic - concurrent separation logic - some extensions of separation logic - program logics for weakly-consistent memory - logics for functional and higher-order languages 2) Selected topics on model checking (3-4 weeks) - model checking - SMT-based model checking - BMC or SAT-based model checking - automata-based model checking 3) Selected topics on language-based software security (3-4 weeks) - typing and security - compilation and security - computing over encrypted or private data - secure multi-party computation

評量方式

Homework 40% Mid-term 30% Final project 30%

教材

【遵守智慧財產權觀念，請使用正版教科書，不得使用非法影印教科書】 使用外文原文書：否 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.