Abstract

Formal verification techniques have seen a remarkable boost in recent years. In particular, methods based on deductive code-verification, model-checking, and code-generation techniques can, within the boundaries of certain foundational assumptions, provide an absolute guarantee in a sense for the correctness of the components of computer based systems towards a specification. However, the assumptions underlying the model, which involves assumptions on the correctness of the compiler, hardware correctness, etc., can cause a significant gap between the specified behavior and the behavior of the code in its execution context. Thus, the verification of the underlying foundational assumptions, ie., the trusted computing base (TCB) is necessary. This can be achieved via prover based testing, where tests are generated from the verified model and executed on the verified code. During my talk, I will introduce a set of applications for this approach, namely, where two formal methods, ie., tests and proofs, are combined together on a top of the interactive theorem proving environment Isabelle.