NSA case study on zero-defect software uses Ada
The National Security Agency has released a case study
showing how to cost-effectively develop code with zero defects. If adopted widely,
the practices advocated in the case study could help make commercial software
programs more reliable and less vulnerable to attack.
The case study used Praxis High Integrity System's
Correctness by Construction techniques, which include programming in the SPARK
subset of Ada.
The project meets or exceeds the Common Criteria Evaluation
Assurance Level (EAL) 5, demonstrating that it is possible to build products that
are reliable, verifiable, and cost effect to this level.
For more information, see
# # #