Hacker-Proof Coding: Software verification helps find the faults, preventing hacks. - Shein, Esther (Communications of the ACM, 2017)
The article discusses coding efforts to avoid hacking by using software verification. Software verification options are discussed including a building tool known as DeepSpec which verifies specifications, the operating system CertiKOS which uses formal verification processes to make sure code behaves as it is intended, without loopholes or bugs, and an optimizing C compiler called CompCert is being evaluated to test fly-by-wire software used by aeronautics company Airbus.