【经典书】计算机科学中的逻辑学:对系统的建模和推理，443页pdf

形式化方法是保证计算机系统正确性与安全性的一种重要方法，其采用数学（逻辑）证明的手段对计算机系统进行建模、规约、分析、推理和验证。

近年来，随着世界各地的公司意识到需要改进验证其产品的手段，验证硬件和软件系统的强大工具得到了发展。对形式推理基本方法的训练要求越来越高，以使学生熟练掌握基于逻辑的验证方法。这本成功的教科书的第二版解决了这两个要求，通过继续提供一个对形式推理的清晰介绍，它既与现代计算机科学的需求相关，又足够严格的实际应用。对第一版的改进已经在整个过程中，与额外的和扩展的章节上的SAT解算器，存在/通用二阶逻辑，微模型，通过契约编程和完全的正确性。模型检查的覆盖范围已经得到了实质性的更新。还增加了进一步的练习。书的互联网支持包括为教师的所有练习的工作的解决方案，和为学生的一些练习的模型解决方案。

http://staff.ustc.edu.cn/~huangwc/book/LogicInCS.pdf