Applications of the methods of proof in CS
- Verification of program correctness
- Establishing that an operating system is secure
- Establishing that certain goals cannot be achieved (such as finding a
universal program-correctness checker or a universal “truth machine”)