Formal verification of spacecraft control programs (experience report)
Andrey Mokhov, Georgy Lukyanov, Jakob Lechner · 2019
Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware.