2 ms·
Rather than knowing your program will work in the sense that a successful compile/execution will tell you, using formal verification you know your program will
by blihp 7y ago
Rather than knowing your program will work in the sense that a successful compile/execution will tell you, using formal verification you know your program will work in the sense that it will do what you want it to do. It's basically programming via logic proofs.
- AnimalMuppet 7y agoCareful there. Not "what you want it to". It will work in the sense that it will do what the formal specification says it will. That may or may not be what you actually want it to do. (MCAS, for example, did what the specification said.)