逻辑与正则验证

Logic and Verification




Information


课程简介

    逻辑是计算机科学中的重要工具,甚至可以认为计算机是在逻辑学基础上构造出来的。本课程主要讲授逻辑学的基本概念和在计算机验证中的应用。计算机验证是计算机科学中的一个重要分支,其开创者(Clarke, Emerson, Sifakis)已经获得了2007年的图灵奖。

    我们将介绍命题逻辑、一阶逻辑、时序逻辑、这些逻辑的相关算法问题(模型检查和可满足性),以及如何应用逻辑来论证计算机软硬件系统的正确性。在本科中,同学们既要进行数学证明,也要进行实际编程。

    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.