A formal proof of properties of a presentation system using Isabelle

摘要

In this paper we present a correctness proof for Infosoft e-Detailing 1.0 presentation software using Isabelle proof assistant. This work illustrates a method of proving correctness of parallel software using proof assistants. Here we concentrate on the state-based approach for proving a safety property. We also give a comparison of this approach with the correctness proof method that was applied to this system in the previous works. The task, rationale, the details of the proof and comparative analysis of approaches are described in this paper.