Re: [isabelle] Verification of C Programs



Maybe a bit more background on that:

Our C-Parser at http://www.ertos.nicta.com.au/software/c-parser/ will translate a large subset of C into the Isabelle/Simpl language,  which comes with various semantics formalisations, verification condition generator, etc.

The version on the website above runs on Isabelle2009-1, we should be able to release the Isabelle2011-1 version shortly, and we're working on the Isabelle2012 update.

The Simpl language is described in Norbert Schirmer's PhD thesis. The C memory model in Harvey Tuch's thesis and a few papers from our web site.

Although the language subset and tool chain are quite powerful and have been applied to large verifications, it is not a very polished tool set at moment, definitely more on the research software side. We'd be happy to help with questions, though.

Cheers,
Gerwin

On 04/06/2012, at 6:49 PM, C. Diekmann wrote:

> 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.