Level: L3
Contact: Burkhart Wolff
Summary.HOL-CSP is a powerful proof-environment based on Isabelle/HOL and the process algebra 'Communicating Sequential Processes' developed by Tony Hoare and Bill Roscoe in the 90ies. In particular, HOL-CSP can model and reason over processes with infinite event structures, so dense time, physical states, algebraic structures, .... Intro FDR4 is a model-checker that provides automated proofs for process-refinements for finite event structures. It is a research question if and to what extent HOL-CSP can be combined with FDR4.
As a prerequisite, the internal presentation of FDR4, a so-called "Labelled Transition System" (LTS) representing CSP processes must be converted into a JSON format that can be read by Isabelle. For this purpose, an internal FDR4 API must be extended by functions that convert the internal LTS data-structure into a JSON output file.
Read the detailed internship proposal.