Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. The progra

Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.