Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-8636
Main Title: Formal Verification of Low-Level Code in a Model-Based Refinement Process (Technical Report: Isabelle/HOL formalization)
Translated Title: Formale Verifikation von Low-Level Programmen im Rahmen eines modellbasierten Verfeinerungsprozesses (Technischer Bericht: Isabelle/HOL Formalisierung)
Author(s): Berg, Nils
Bartels, Björn
Danziger, Armin
Grochau Azzi, Guilherme
Bentert, Matthias
Type: Report
Language Code: en
Abstract: 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.
URI: https://depositonce.tu-berlin.de/handle/11303/9591
http://dx.doi.org/10.14279/depositonce-8636
Issue Date: Sep-2019
Date Available: 19-Sep-2019
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): Isabelle/HOL
Hoare logics
refinement
Communicating Sequential Processes
unstructured code
License: https://choosealicense.com/licenses/mit/
Appears in Collections:Inst. Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
berg_etal_Isabelle-HOL-formalization.pdf132.35 kBAdobe PDFThumbnail
View/Open
CUC.zipIsabelle HOL Formalization465.97 kBZIP ArchiveView/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.