[isabelle] Verification of C Programs

What is the best approach for verifying the correctness of C programs in 
Isabelle? I see that some people have done some work on this already, but 
is there a current best approach?  This is for a virtual machine/assembly 
language that is implemented in C and will be used as the target language 
for a compiler that will need to be verified in Isabelle as well.  I 
would like to verify the implementation of the virtual machine.

Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.

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