华保健编著

图书介绍

形式化方法是计算机科学理论中历史悠久、理论性强、发展成熟的学科，已发展成为计算机 科学的重要分支之一。形式化方法主要用数学的理论和工具，对计算机软硬件系统进行形式建模和性质推理研究，以期证明系统的实现正确性，或提高系统的可靠性和健壮性等。本书全面讲授形式化方法理论及应用，从基础知识出发，讨论了数理逻辑、可满足性、决策过程以及理论应用等内容，并给出了丰富的实例。全书共分为 13 章，分别讨论了理论基础、命题逻辑、布尔可满足性、谓词逻辑、可满足性模理 论、数据结构的判定、符号执行、程序验证、程序合成、Curry-Howard同构、依赖类型等内容，并给出了充分的实践讨论与应用实例。