Focus on Isabelle: From specifcation to verifcation
Maria Spichkova · RMIT Research Repository (RMIT University Library) · 2008
This approach introduces a coupling of a specification framework with a verification system. Given a system, represented in a formal specification framework, one can verify its properties by translating the specification to a Higher-Order Logic and subsequently using the theorem prover Isabelle/HOL or the point of disagreement will be found. Moreover, using this approach one can validate the refinement relation between two given systems, as well as make automatic correctness proofs of syntactic interfaces for specified system components. The approach uses particularly the idea of refinement-based verification, where a verification of system properties can be treated as a validation of a system specification with respect to the specification of the properties.