| Topic | Application | Reference Links |
|---|---|---|
| Program proofs | Automatic program provers: In many critical software industries, like space, defense, healthcare, one would have to prove programs for safety and liveness. One would have to do this for a range of expected inputs. | A great high level article is "Program Verification: Vision and Reality" in CACM 2021. |
| Induction and its related cousin, Recurrences | It has been used to explain several effects in nature or human society. Examples: 1. Domino effect 2. Counting the number of handshakes in a room (could be useful if you are a popular politician) 3. Estimating how the population will grow (or in the case of some unfortunate countries, shrink)
|
|
| Program verification | This is widely used in the industry. One concrete use case is in verification of the design of integrated circuits, that they meet timing or race condition checks. The Turing Award (~ Nobel Prize of computing) went for "Model checking" a close cousin, in 2007. |
Turing award lecture by Joseph Sifakis, 2007, titled "The Quest for Correctness beyond Verification". |