Program Verification

Mathematical Logic · Axiom Academy

REAL WORLD Program Verification How First-Order Logic proves software is correct and saves lives In 1996, the Ariane 5 rocket exploded 37 seconds after launch, destroying a 370 million payload. The cause? A software bug—a 64-bit floating point number was converted to a 16-bit integer, causing an overflow. This catastrophic failure could have been prevented by formal verification. The answer: Use first-order logic to reason about program behavior. Software controls critical systems: aircraft autopilots, medical devices, nuclear reactors, autonomous vehicles. Testing alone isn't enough—testing shows the presence of bugs, not their absence. We need mathematical proof that programs are correct. Hoare Logic: Reasoning About Programs A Hoare triple is a statement about program correctness written as: is the precondition (what must be true before) is the postcondition (what will be true after) This means: "If is true before executing , and terminates, then will be true afterward." Consider this program that increments a variable: We can specify its correctness with a Hoare triple: This states: "If before the command, then after." This is a mathematical proof that the program correctly increments the variable. Program Specifications with FOL First-order logic provides the language for writing preconditions and postconditions. We use: Properties of variables and states Universal and existential statements Loop Invariants: The Key to Verification

This is the written version of the interactive lesson above. See the full Mathematical Logic course.