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