Thumbnail Image

Formal Verification of Low-Level Code in a Model-Based Refinement Process (Technical Report: Isabelle/HOL formalization)

Berg, Nils; Bartels, Björn; Danziger, Armin; Grochau Azzi, Guilherme; Bentert, Matthias

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.