INTRODUCTION

Objectives

• Assist verification engineers by providing an easy-to-use Web platform for proof requests and overview the current verification flow.
• Analyze logical dependencies within verification projects and relations within the whole verification process.
• Optimize Isabelle/HOL theory files under provided conditions.
• Extend the existing Web interface for collecting and managing the proof requests.

Dependencies

Wile verifying a large system, proof of a single lemma is usually based on a number of previously proven lemmas. These dependency relations can be described described in the form of a Graph data structure.

Example: Dependencies within the verification of FlexRay Communication Protocol, a time-triggered protocol developed for automotive systems.

In the program, an application is developed to analyze the verification structure and generate excel files of results.