Re: [isabelle] Verification of C Programs



Maybe this mail is helpful:
Subject: "L4.verified C-to-Isabelle parser release"
Date: Wed, 14 Dec 2011 17:13:17 +1100
From: Gerwin Klein
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-December/msg00014.html

2012/6/4 Aaron W. Hsu <arcfide at sacrideo.us>:
> 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.