Tag: formal-verification

George Necula's proof-carrying code shifted trust toward machine-checkable evidence: untrusted code could arrive with a proof that it satisfied a receiver-defined safety policy.

Per Martin-Löf's intuitionistic type theory made types expressive enough to depend on values, linking programs, mathematical propositions, and constructive proofs in one formal language.

ACL2 turned the Boyer-Moore tradition of automated inductive theorem proving into an executable Common Lisp-based logic that could model and verify commercial hardware and software systems.

NuSMV reengineered the pioneering SMV model checker into an open, modular verification platform that combined symbolic state-space reasoning with a tool architecture suitable for research and industrial experimentation.

Bounded model checking recast finite-depth verification as Boolean satisfiability, using rapidly improving SAT solvers to find deep counterexamples without constructing a global symbolic state representation.

Lawrence Paulson designed Isabelle as a generic proof assistant in which different object logics could be represented inside one trusted framework, later developing Isabelle/HOL into a major environment for formal mathematics and verification.

SPARK evolved from a restricted Ada subset into a verification-oriented language and toolchain designed to make data flow, contracts and proof usable in safety- and security-critical software projects.

Hoare logic organized program proofs around preconditions, commands and postconditions, creating a compositional calculus that still shapes verification tools and software contracts.

Amir Pnueli brought temporal logic into program verification, giving concurrent and reactive systems a language for safety, liveness and behavior across time.

seL4 connected a high-performance microkernel implementation to a formal specification with machine-checked proofs, pushing software verification into the privileged operating-system core.