Verifying Launch Interceptor Routines With the Asymptotic Method.
UNISYS CORP RESTON VA RESTON TECHNOLOGY CENTER
Pagination or Media Count:
This report describes the results of an exercise in formal program verification conducted at ORA. In this exercise, we started with code written by students at Syracuse University as part of work conducted by Professor Amrit Goel on program development methods. The code was an implementation of the routines of the Launch Interceptor Program LIP, a specification of a protocol for launching an interceptor missile. This specification was used by Knight and Leveson in a well-known experiment in N-version programming.
- Antimissile Defense Systems