Loading...
Please wait, while we are loading the content...
Similar Documents
Embedding and verification of an mdg-hdl translator in hol (2000).
| Content Provider | CiteSeerX |
|---|---|
| Author | Xiong, Haiyan Curzon, Paul Tahar, Sofiène Blandford, Ann |
| Abstract | We investigate the verification of a translation phase of the Multiway Decision Graphs (MDG) verification system using the Higher Order Logic (HOL) theorem prover. In this paper, we deeply embed the semantics of a subset of the MDG-HDL language and its Table subset into HOL. We define a set of functions which translate this subset MDG-HDL language to its Table subset. A correctness theorem for this translator, which quantifies over its syntactic structure, has been proved. This theorem states that the semantics of the MDG-HDL program is equivalent to the semantics of its Table subset. |
| File Format | |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | Mdg-hdl Translator Table Subset Mdg-hdl Language Subset Mdg-hdl Language Translation Phase Theorem Prover Multiway Decision Graph Mdg-hdl Program Order Logic Verification System Correctness Theorem Theorem State Syntactic Structure |
| Content Type | Text |
