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



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?

  -- Lars





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