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:
>> The parser reads .c files after preprocessing and translates them into the language Simpl by Norbert Schirmer embedded in Isabelle/HOL []. 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.


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