the echo approach to formal verification
In this research abstract, we propose Echo: a general formal verification approach that combines theorem proving, model checking, and code-level tools to show an implementation's compliance with its formal specification. We believe that this approach is novel since the major proof step is carried out between two abstract specification models, thus avoiding or mitigating the difficulty of the direct compliance proof of a concrete implementation against an abstract formal specification in traditional Floyd-Hoare verification. We present our prototype design and implementation of the major components of the approach and we instantiate the approach to verify SPARK Ada implementations against PVS specifications. We conducted an initial experiment to determine the feasibility of the approach using a hypothetical avionics system.
formal verification formal specification