Formal Verification

Definition / 定义

形式化验证：用严格的数学方法（如逻辑证明、模型检查等）来证明或反驳一个系统（软件、硬件、协议）是否满足其形式化规格说明，以获得比测试更强的正确性保证。（也常简称为“formal methods”的核心应用之一。）

Pronunciation / 发音

/ˈfɔːrməl ˌvɛrɪfɪˈkeɪʃən/

Examples / 例句

Formal verification can prove that a circuit meets its safety requirements.
形式化验证可以证明一个电路满足其安全性要求。

Because concurrency bugs are hard to reproduce, the team used formal verification to mathematically verify the protocol’s liveness and absence of deadlock under all possible schedules.
由于并发错误很难复现，团队采用形式化验证，从数学上证明该协议在所有可能的调度下都满足活性并且不会死锁。

Etymology / 词源

formal 来自拉丁语 formalis（“形式的、与形状/结构相关的”），强调“按规则、按形式系统”进行；verification 来自拉丁语 verus（“真实的”）与 facere（“做、使成”）的组合，经由法语演变为英语，意为“使之被确认为真”。合起来的 formal verification 强调“用形式系统把‘真实/正确’确定下来”。在计算机科学中，这类思想与程序正确性证明（如 Hoare 逻辑）和后来的模型检查等方法密切相关。

Related Words / 相关词

• Model Checking
• Theorem Proving
• Static Analysis
• Specification
• Correctness
• Proof
• Temporal Logic
• Hoare Logic
• SAT Solving

Literary Works / 文学作品

• Model Checking（Clarke, Grumberg, Peled）
• Principles of Model Checking（Baier & Katoen）
• Software Abstractions: Logic, Language, and Analysis（Daniel Jackson，涉及 Alloy 与形式化分析/验证）
• The Temporal Logic of Reactive and Concurrent Systems（Zohar Manna & Amir Pnueli，常与形式化验证语境并用）
• Computer-Aided Verification (CAV) Proceedings（会议论文集中频繁出现 “formal verification” 用语）