Verification of Sequential Imperative Programs in Isabelle/HOL

摘要: The purpose of this thesis is to create a verification environment for sequential imperative programs. First general language model proposed, which independent concrete programming but expressive enough cover all common features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local global variables, pointers heap, expressions with side effects, partial application closures, dynamic method invocation also unbounded nondeterminism. For Hoare logic both total correctness developed on top it condition generator implemented. designed allow the integration program analysis or software checking into verification. To demonstrate continuity real subset C embedded environment. whole work in theorem prover Isabelle. Therefore machine-checked addition rich infrastructure Isabelle can be employed