Re: [isabelle] L4.verified C-to-Isabelle parser release



On 04/01/2012, at 10:23 PM, Lars Noschinski wrote:

> On 14.12.2011 07:13, Gerwin Klein wrote:
>> We're pleased to announce the release of the C-to-Isabelle/Simpl parser by Michael Norrish that was used in the L4.verified project.
>> 
>> It is available for download under BSD license from:
>> http://www.ertos.nicta.com.au/software/c-parser/
>> 
>> The parser reads .c files after preprocessing and translates them into the language Simpl by Norbert Schirmer embedded in Isabelle/HOL [http://afp.sf.net/entries/Simpl.shtml]. Programs in Simpl can then be verified using the VCG and other mechanisms of that package.
>> 
>> This release is still very much a research tool for experts and is based on Isabelle2009-1. We are aiming at porting the parser to the current Isabelle version in the future.
> 
> Do you have any estimate when this is going to happen or how much of an effort it will be to port this to a current Isabelle version?

We're looking at updating all our proofs in the next 2 months or so (optimistically). That includes the parser.

Effort: the C parser is usually one of the more painful parts, because it uses ML-level Isabelle APIs which tend to change a lot more than the user level. We might be pestering people with questions in a few weeks on new ways of doing things.

Cheers,
Gerwin






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