Patrick and Radhia Cousot gave static analysis a mathematical foundation in which program behavior is safely approximated in abstract domains, making automated proofs possible without enumerating every execution.
Separation logic extended Hoare-style program reasoning with spatial connectives that let proofs describe disjoint pieces of memory, enabling local reasoning about pointers and later scalable automated analysis.
Rustan Leino’s Dafny made specifications, executable code and automated verification part of one programming language, using Boogie and SMT solving to check functional correctness as developers write programs.
Robert Floyd's assertion method turned program correctness into a mathematical problem by attaching logical conditions to control flow and proving that execution preserves them.