| 课程号 |
04833260 |
学分 |
2 |
| 英文名称 |
Logic and Verification |
| 先修课程 |
无 |
| 中文简介 |
本科的授课教师为英国牛津大学的Anthony W. Lin教授。
逻辑是计算机科学中的重要工具，甚至可以认为计算机是在逻辑学基础上构造出来的。本课程主要讲授逻辑学的基本概念和在计算机验证中的应用。计算机验证是计算机科学中的一个重要分支，其开创者(Clarke, Emerson, Sifakis)已经获得了2007年的图灵奖。
我们将介绍命题逻辑、一阶逻辑、时序逻辑、这些逻辑的相关算法问题（模型检查和可满足性），以及如何应用逻辑来论证计算机软硬件系统的正确性。在本科中，同学们既要进行数学证明，也要进行实际编程。
注：课程的中文名称应为《逻辑与程序验证》。原课程名称系繁体中文翻译错误。 |
| 英文简介 |
This course will be taught by Prof. Anthony W. Lin from Oxford.
Logic is an indispensable tool in computer science and is used in every facet of the field. One may even argue that computers are built on top of logic (logic gates are the basic building blocks of computers). This course introduces fundamental concepts in logic in computer science with applications in algorithmic verification of computer systems, a field that was pioneered by 2007 Turing Award Winners (Clarke, Emerson, and Sifakis).
We will discuss propositional logic, first-order logic, temporal logics, their basic algorithmic problems (e.g. model checking and satisfiability), and how they can be applied for reasoning about computer systems (hardware, software, etc.). The course requires students to do both mathematical proofs and programming.
|
| 开课院系 |
信息科学技术学院 |
| 通选课领域 |
|
| 是否属于艺术与美育 |
否 |
| 平台课性质 |
|
| 平台课类型 |
|
| 授课语言 |
英文 |
| 教材 |
Logic in Computer Science,Michael Huth and Mark Ryan,Cambridge University Press,2004,Model Checking,Edmund Clarke, Orna Grumberg, and Doron,MIT Press,2000,Logic and Structure,Dirk van Dalen,Springer,2008,Handbook of Knowledge Representation (Chapter 2),F. van Harmelen, V. Lifschitz, and B. Porter,Elsevier,2008,Theory of Computation,Dexter Kozen,Springer,2006,The Calculus of Computation,Aaron Bradley and Zohar Manna,Springer,2007,System and Software Verification,Berard and Bidoit,Springer,2001,Z3py Tutorial (https://github.com/ericpony/z3py-tutorial),Z3 team,Principles of Model Checking,Christel Baier and Joost-Pieter Katoen,MIT Press,2008,Semantics with Applications,Hanne Riis Nielson and Flemming Nielson,Springer,2007,Rigorous Software Development: An Introduction to Software Verification,José Bacelar Almeida, et al.,Springer,2011,Elements of Finite Model Theory,Leonid Libkin,Springer,2004,Languages, Automata, and Logic (in Handbook of formal languages, vol. 3),Woflgang Thomas,Springer-Verlag,1997, |
| 参考书 |
|
| 教学大纲 |
1. Understanding the role of logic and how to use it for formally reasoning about computational processes。
2. Being able to apply automatic tools from logic and verification (e.g. SAT-solvers) to solve interesting reasoning problems (e.g. Sudoku).
* Propositional Logic:
o Syntax, semantics, substitution, normal forms, equivalences (3)
o Satisfiability, getting familiar with a SAT-solver, application in constraint solving and verification (4)
o Decision procedures for satisfiability (4)
* First-Order Logic:
o Syntax, semantics, substitution, normal forms, equivalences (3)
o Satisfiability, model checking, undecidability (2)
* Temporal Logic (Linear Temporal Logic and Computation Tree Logic)
o Syntax, semantics, modelling systems (3)
o Model checking algorithms, getting familiar with a model checker, application in verification (4)
* First-Order Theories and Program Verification (7):
o Satisfiability Modulo Theories (SMT) and SMT-solvers
o Theory of Linear Arithmetic
o Operational Semantics, Hoare Logic, and Application to Program Verification
* Student presentations (2)
课堂授课为主，课后读论文、做调研及汇报为辅。
Presentation（10%），Project（40%），Final Take-Home Exam（50％）
|
| 教学评估 |
熊英飞：
学年度学期：16-17-3，课程班：逻辑和程序验证1，课程推荐得分：5.0，教师推荐得分：5.0，课程得分分数段：100-105；
|
|