Mechanical Software Verification: High Level Control Aspects from a User's Perspective

We present lessons learned from using mechanical theorem proving for proof support in software verification, with trusted execution of programs in mind. We will use two realistic running examples, compiler verification, which is central if we want to prove that we can trust a piece of executable software, and an industrial project in which we proved the correctness of a safety critical expert system using (verified) runtime result verification. We will emphasize the role of partial program correctness and its preservation. And we will comment on high level control aspects, in particular on what we can and what we will not be able to prove for a concrete piece of executable software.