本书系统介绍了各种可判定的一阶理论及其在自动软件和硬件验证、定理证明与编译器优化等场景中的具体应用，涵盖了可满足性（SAT）求解器和可满足性模理论（SMT）求解器的核心技术，以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题，并借助高效的判定过程进行求解。本书不仅为研究人员提供了丰富的理论知识，还为高级软件工程师和开发者提供了实用的参考指南。

本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读。

Daniel Kroening是牛津大学计算机科学系的教授，他的兴趣包括自动验证、软件工程和编程语言。 Ofer Strichman是以色列理工学院工业工程与管理学院的教授，他的研究兴趣包括软件和硬件的形式化验证，以及一阶逻辑片段的决策程序。