Formale Verifikation von Low-Level Programmen im Rahmen eines modellbasierten Verfeinerungsprozesses (Technischer Bericht: Isabelle/HOL Formalisierung)

This is the technical report for the Isabelle/HOL formalization accompanying the dissertation of Nils Berg. For explanations with regard to content please refer to the dissertation. The intention of this document is to give a mapping from the formalization in the dissertation to the formalization in Isabelle/HOL. Formalized are the parts where user interaction is required, i.e., the first part of the dissertation, where Communicating Sequential Processes (CSP) processes and Communicating Unstructured Code (CUC) programs are related. More specifically, the sections 5.2 to 5.5 of the dissertation are formalized