授课教师：Zhe Hou

国籍：澳大利亚

职称：副教授

教师简介（中英文）：Zhe Hou 获得了澳大利亚国立大学的博士学位。他开发了多种自动推理技术和工具，用于分离逻辑——一种用于推理具有指针和其他可变数据结构的计算机程序的逻辑。2015年，他加入了新加坡南洋理工大学，参加了“Securify”项目，在该项目中，他为SPARCv8指令集架构和TSO弱内存模型开发了正式模型，并验证了正式模型的信息流安全性。2017年，他加入了澳大利亚格里菲斯大学，参与了与澳大利亚国防科技合作开发可信自主系统和先进的模型检查技术的项目。他于2019年底加入格里菲斯大学的教职。

Zhe Hou obtained his PhD from the Australian National University. He has developed various automated reasoning techniques and tools for separation logic -- a logic for reasoning about computer programs with pointers and other mutable data structures. In 2015 he joined Nanyang Technological University, Singapore, to undertake the project "Securify", in which he developed formal models of the SPARCv8 instruction set architecture and TSO weak memory model, and verified information-flow security for the formal models. He joined Griffith University, Australia, in 2017 on a project to develop trusted autonomous systems and advanced model checking techniques in collaboration with Australia Defense Science and Technology. He joined the faculty at Griffith University in late 2019.

课程简介（中英文）：这门课程介绍了逻辑和推理的基本原理，包括经典逻辑和非经典逻辑的语法、语义和证明理论。它还涵盖了形式语言、自动机理论和计算理论。最后，它通过使用Curry-Howard对应关系来讨论逻辑和计算之间的关系。本课程的前半部分配有Isabelle/HOL的练习，Isabelle/HOL是一种流行且用户友好的定理证明器。本课程的后半部分涉及使用过程分析工具包（PAT）进行建模和验证，PAT是一种基于Hoare的通信顺序过程的功能丰富的模型检查器。本书还提供了Isabelle/HOL和PAT的入门教程。实用定理证明和模型检查的混合技能对读者未来的研究或形式方法工程师的职业发展都有帮助。

This course introduces the fundamentals of logic and reasoning, including the syntax, semantics and proof theory of classical logic and non-classical logics. It also covers formal languages, automata theory and the theory of computation. Finally, it discusses the relationship between logic and computation using the Curry-Howard Correspondence. The first half of the course is accompanied by exercises in Isabelle/HOL, which is a popular and user-friendly theorem prover. The second half of the course involves modelling and verification in Process Analysis Toolkit (PAT), a feature-rich model checker based on Hoare’s Communicating Sequential Processes. This book also provides entry-level tutorials for Isabelle/HOL and PAT. The hybrid skill set of practical theorem proving and model checking should be helpful for the future of readers should they pursue a research career or engineering in formal methods.