Engineering Self-Verified Software
Implementation and verification are traditionally viewed as two separate activities. Even in test-driven environments, the test platform is distinct from the implementation one. This talk will present an alternative approach where the verification and development activities are engineered together, creating effectively a “self-verified” program combining at the same place an implementation and the means to verify its correctness.
4 key takeaways
- Developing verification at the same time as the code allows for more efficient coding processes and mitigates errors at the end of the process.
- Formal proofs and testing can be combined to increase the level of safety and decrease overall development costs.
- There are alternatives to the C programming language that allows more effective verification.
- There is a way to redirect software developers energy from worrying about low-level coding errors to concentrate on more valuable aspects of software engineering