%0 Journal Article %1 loepucl5153 %A Xiong, H.Y. %A Curzon, P. %A Tahar, S. %A Blandford, A. %D 2007 %J Formal Methods in System Design %K Formal-hardware-verification Verification-system-correctness hybrid-verification-systems usability-verification %N 2 %P 83--116 %T Providing a formal linkage between MDG and HOL %U http://eprints.ucl.ac.uk/5153/ %V 30 %X We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation part of the symbolic state system. It interfaces between low level decision diagrams and high level description languages. We ensure that the semantics of a program is preserved in those of its translated form. Secondly we prove linkage theorems: theorems that justify introducing a result from a state enumeration system into a proof system. Finally we combine the translator correctness and linkage theorems. The resulting new linkage theorems convert results to a high level language from the low level decision diagrams that the result was actually proved about in the state enumeration system. They justify importing low-level external verification results into a theorem prover. We use a linkage between the HOL system and a simplified version of the MDG system to illustrate the ideas and consider a small example that integrates two applications from MDG and HOL to illustrate the linkage theorems.

@article{loepucl5153, abstract = {We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation part of the symbolic state system. It interfaces between low level decision diagrams and high level description languages. We ensure that the semantics of a program is preserved in those of its translated form. Secondly we prove linkage theorems: theorems that justify introducing a result from a state enumeration system into a proof system. Finally we combine the translator correctness and linkage theorems. The resulting new linkage theorems convert results to a high level language from the low level decision diagrams that the result was actually proved about in the state enumeration system. They justify importing low-level external verification results into a theorem prover. We use a linkage between the HOL system and a simplified version of the MDG system to illustrate the ideas and consider a small example that integrates two applications from MDG and HOL to illustrate the linkage theorems.}, added-at = {2008-10-24T14:29:07.000+0200}, author = {Xiong, H.Y. and Curzon, P. and Tahar, S. and Blandford, A.}, biburl = {https://www.bibsonomy.org/bibtex/294c56d0895b952b0a45e54032f24f29a/uclic}, description = {UCLIC eprints as of October 2008}, interhash = {7b5d6e004090e19ab1d5ef5042732483}, intrahash = {94c56d0895b952b0a45e54032f24f29a}, journal = {Formal Methods in System Design}, keywords = {Formal-hardware-verification Verification-system-correctness hybrid-verification-systems usability-verification}, month = {April}, note = {The original publication is available at www.springerlink.com}, number = 2, pages = {83--116}, timestamp = {2008-10-24T14:49:06.000+0200}, title = {Providing a formal linkage between MDG and HOL}, url = {http://eprints.ucl.ac.uk/5153/}, volume = 30, year = 2007 }