Re: [isabelle] do hardware verification by Isabelle



li yongjian wrote:
Hi,
   I want to know who has done some theorem proof work on
hardware verification by using Isabelle.

   I know HOL has been extensively used in harware by Mike
Gordon, Tom mellem, and so on. There are large nuber of papers,
 case studies, proofs
   But I found little  work which does harware verification by
Isabelle.
   By google search, I found larry's old project introduction:
Combining HOL with Isabelle. But I can not find intereting papers
on this field.

   I fact, I have a HOL proof theories which I'm interested  in, but
I'm not familar with HOL. Do I need rewrite a new version of
Isabelle script basing on the HOL, or learn  HOL to do harware verification.

regards!


The L4 project includes substantial hardware verification, and there are papers about that, including my

Jeremy E. Dawson, Isabelle Theories for Machine Words. In Seventh International Workshop on Automated Verification of Critical Systems (AVOCS'07), Oxford, September 2007, Electronic Notes in Theoretical Computer Science, Elsevier, to appear. (Also in Proceedings of TPHOLs 2007 Emerging Trends, Internal Report 364/07, Department of Computer Science, University of Kaiserslautern)

On-line at http://users.rsise.anu.edu.au/~jeremy/pubs/l4/

Jeremy






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.